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

Theorem ceqsalv 3448
 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 1915 . 2 𝑥𝜓
2 ceqsalv.1 . 2 𝐴 ∈ V
3 ceqsalv.2 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
41, 2, 3ceqsal 3447 1 (∀𝑥(𝑥 = 𝐴𝜑) ↔ 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1536   = wceq 1538   ∈ wcel 2111  Vcvv 3409 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-12 2175 This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2736  df-clel 2830 This theorem is referenced by:  ralxpxfr2d  3557  clel4OLD  3577  frsn  5608  raliunxp  5679  idrefALT  5945  funimass4  6718  marypha2lem3  8934  kmlem12  9621  vdwmc2  16370  itg2leub  24434  nmoubi  28654  choc0  29208  nmopub  29790  nmfnleub  29807  fnssintima  33194  elintfv  33254  eqscut2  33561  heibor1lem  35527  elmapintrab  40649
 Copyright terms: Public domain W3C validator