MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ceqsalv Structured version   Visualization version   GIF version

Theorem ceqsalv 3511
Description: A representation of explicit substitution of a class for a variable, inferred from an implicit substitution hypothesis. (Contributed by NM, 18-Aug-1993.) Avoid ax-12 2170. (Revised by SN, 8-Sep-2024.)
Hypotheses
Ref Expression
ceqsalv.1 𝐴 ∈ V
ceqsalv.2 (𝑥 = 𝐴 → (𝜑𝜓))
Assertion
Ref Expression
ceqsalv (∀𝑥(𝑥 = 𝐴𝜑) ↔ 𝜓)
Distinct variable groups:   𝑥,𝐴   𝜓,𝑥
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem ceqsalv
StepHypRef Expression
1 19.23v 1944 . 2 (∀𝑥(𝑥 = 𝐴𝜓) ↔ (∃𝑥 𝑥 = 𝐴𝜓))
2 ceqsalv.2 . . . 4 (𝑥 = 𝐴 → (𝜑𝜓))
32pm5.74i 271 . . 3 ((𝑥 = 𝐴𝜑) ↔ (𝑥 = 𝐴𝜓))
43albii 1820 . 2 (∀𝑥(𝑥 = 𝐴𝜑) ↔ ∀𝑥(𝑥 = 𝐴𝜓))
5 ceqsalv.1 . . . 4 𝐴 ∈ V
65isseti 3489 . . 3 𝑥 𝑥 = 𝐴
76a1bi 362 . 2 (𝜓 ↔ (∃𝑥 𝑥 = 𝐴𝜓))
81, 4, 73bitr4i 303 1 (∀𝑥(𝑥 = 𝐴𝜑) ↔ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wal 1538   = wceq 1540  wex 1780  wcel 2105  Vcvv 3473
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107
This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-clel 2809
This theorem is referenced by:  ceqsexv  3525  ralxpxfr2d  3634  clel4OLD  3654  frsn  5763  raliunxp  5839  idrefALT  6112  funimass4  6956  fnssintima  7362  imaeqalov  7649  marypha2lem3  9435  kmlem12  10159  vdwmc2  16917  itg2leub  25485  eqscut2  27545  addsuniflem  27724  mulsuniflem  27844  nmoubi  30293  choc0  30847  nmopub  31429  nmfnleub  31446  elintfv  35041  heibor1lem  36981  elmapintrab  42630
  Copyright terms: Public domain W3C validator