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

Theorem ceqsalv 3480
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 2172. (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 1946 . 2 (∀𝑥(𝑥 = 𝐴𝜓) ↔ (∃𝑥 𝑥 = 𝐴𝜓))
2 ceqsalv.2 . . . 4 (𝑥 = 𝐴 → (𝜑𝜓))
32pm5.74i 271 . . 3 ((𝑥 = 𝐴𝜑) ↔ (𝑥 = 𝐴𝜓))
43albii 1822 . 2 (∀𝑥(𝑥 = 𝐴𝜑) ↔ ∀𝑥(𝑥 = 𝐴𝜓))
5 ceqsalv.1 . . . 4 𝐴 ∈ V
65isseti 3459 . . 3 𝑥 𝑥 = 𝐴
76a1bi 363 . 2 (𝜓 ↔ (∃𝑥 𝑥 = 𝐴𝜓))
81, 4, 73bitr4i 303 1 (∀𝑥(𝑥 = 𝐴𝜑) ↔ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wal 1540   = wceq 1542  wex 1782  wcel 2107  Vcvv 3444
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-clel 2816
This theorem is referenced by:  ceqsexv  3493  ralxpxfr2d  3595  clel4OLD  3615  frsn  5718  raliunxp  5794  idrefALT  6064  funimass4  6905  fnssintima  7304  marypha2lem3  9332  kmlem12  10056  vdwmc2  16811  itg2leub  25051  eqscut2  27097  nmoubi  29543  choc0  30097  nmopub  30679  nmfnleub  30696  imaeqalov  34108  elintfv  34149  addsunif  34301  heibor1lem  36200  elmapintrab  41753
  Copyright terms: Public domain W3C validator