diff --git a/iris/program_logic/total_weakestpre.v b/iris/program_logic/total_weakestpre.v
index 5dadf421fd2816d089a3115d8fdb20c86a7b7abe..c196e5c9078eb38af1f599498d6fd83a47417bb8 100644
--- a/iris/program_logic/total_weakestpre.v
+++ b/iris/program_logic/total_weakestpre.v
@@ -303,4 +303,8 @@ Section proofmode_classes.
   Global Instance add_modal_fupd_twp s E e P Φ :
     AddModal (|={E}=> P) P (WP e @ s; E [{ Φ }]).
   Proof. by rewrite /AddModal fupd_frame_r wand_elim_r fupd_twp. Qed.
+
+  Global Instance into_fupd_twp E e s Φ :
+    IntoFUpd E (WP e @ s; E [{ Φ }]) (WP e @ s; E [{ Φ }]).
+  Proof. apply fupd_intro. Qed.
 End proofmode_classes.
diff --git a/iris/program_logic/weakestpre.v b/iris/program_logic/weakestpre.v
index c10cd66f564f7083d3a6276ffbcd5a7042dd39a1..a532b7031668873a30049e2d824311f8f79e6735 100644
--- a/iris/program_logic/weakestpre.v
+++ b/iris/program_logic/weakestpre.v
@@ -321,4 +321,8 @@ Section proofmode_classes.
     iApply (wp_wand with "(Hinner Hα)").
     iIntros (v) ">[Hβ HΦ]". iApply "HΦ". by iApply "Hclose".
   Qed.
+
+  Global Instance into_fupd_wp E e s Φ :
+    IntoFUpd E (WP e @ s; E {{ Φ }}) (WP e @ s; E {{ Φ }}).
+  Proof. apply fupd_intro. Qed.
 End proofmode_classes.
diff --git a/iris/proofmode/class_instances_updates.v b/iris/proofmode/class_instances_updates.v
index 5fd7fea8bda20e776893c76b74852bc4a532b877..232efd3c926b2476e90ebbbe554acfd974de1f68 100644
--- a/iris/proofmode/class_instances_updates.v
+++ b/iris/proofmode/class_instances_updates.v
@@ -178,4 +178,11 @@ Proof.
   iMod ("Hinner" with "Hα") as "[Hβ Hfin]".
   iMod ("Hclose" with "Hβ") as "Hγ". by iApply "Hfin".
 Qed.
+
+Global Instance into_fupd_default `{!BiFUpd PROP} E P :
+  IntoFUpd E (|={E}=> P) P | 100.
+Proof. by rewrite /IntoFUpd. Qed.
+Global Instance into_fupd_fupd `{!BiFUpd PROP} E1 E2 P :
+  IntoFUpd E1 (|={E1,E2}=> P) (|={E1,E2}=> P) | 1.
+Proof. apply fupd_intro. Qed.
 End class_instances_updates.
diff --git a/iris/proofmode/classes.v b/iris/proofmode/classes.v
index dd4c2a2c6830d23c42d9e77d959e71062c23ca3b..0bf229bad2e965ba1f5eee0ec8b5ea20b159b8d2 100644
--- a/iris/proofmode/classes.v
+++ b/iris/proofmode/classes.v
@@ -1,5 +1,5 @@
 From stdpp Require Import namespaces.
-From iris.bi Require Export bi.
+From iris.bi Require Export bi updates.
 From iris.proofmode Require Import base.
 From iris.proofmode Require Export ident_name modalities.
 From iris.prelude Require Import options.
@@ -263,6 +263,16 @@ Global Hint Mode AddModal + - ! ! : typeclass_instances.
 Lemma add_modal_id {PROP : bi} (P Q : PROP) : AddModal P P Q.
 Proof. by rewrite /AddModal wand_elim_r. Qed.
 
+(** The [into_fupd E P Q] class is used to add an [|={E}=>] modality to the
+proposition [Q].
+
+The input are [E] and [Q], the output is [P]. *)
+Class IntoFUpd `{!BiFUpd PROP} E (P Q : PROP) :=
+  into_fupd : P ={E}=∗ Q.
+Arguments IntoFUpd {_ _} _ _%I _%I : simpl never.
+Arguments into_fupd {_ _} _ _%I _%I {_}.
+Global Hint Mode IntoFUpd + + ! - ! : typeclass_instances.
+
 (** We use the classes [IsCons] and [IsApp] to make sure that instances such as
 [frame_big_sepL_cons] and [frame_big_sepL_app] cannot be applied repeatedly
 often when having [ [∗ list] k ↦ x ∈ ?e, Φ k x] with [?e] an evar. *)