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

Theorem ceqsalv 3537
Description: A representation of explicit substitution of a class for a variable, inferred from an implicit substitution hypothesis. (Contributed by NM, 18-Aug-1993.)
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 nfv 1908 . 2 𝑥𝜓
2 ceqsalv.1 . 2 𝐴 ∈ V
3 ceqsalv.2 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
41, 2, 3ceqsal 3536 1 (∀𝑥(𝑥 = 𝐴𝜑) ↔ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wal 1528   = wceq 1530  wcel 2106  Vcvv 3499
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2108  ax-9 2116  ax-12 2167  ax-ext 2796
This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1083  df-ex 1774  df-nf 1778  df-cleq 2817  df-clel 2897
This theorem is referenced by:  ralxpxfr2d  3642  clel4  3659  frsn  5637  raliunxp  5708  idrefALT  5970  funimass4  6726  marypha2lem3  8893  kmlem12  9579  vdwmc2  16307  itg2leub  24250  nmoubi  28464  choc0  29018  nmopub  29600  nmfnleub  29617  elintfv  32892  heibor1lem  34956  elmapintrab  39798
  Copyright terms: Public domain W3C validator