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

Theorem vtoclf 3544
Description: Implicit substitution of a class for a setvar variable. This is a generalization of chvar 2415. (Contributed by NM, 30-Aug-1993.)
Hypotheses
Ref Expression
vtoclf.1 𝑥𝜓
vtoclf.2 𝐴 ∈ V
vtoclf.3 (𝑥 = 𝐴 → (𝜑𝜓))
vtoclf.4 𝜑
Assertion
Ref Expression
vtoclf 𝜓
Distinct variable group:   𝑥,𝐴
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)

Proof of Theorem vtoclf
StepHypRef Expression
1 vtoclf.1 . . 3 𝑥𝜓
2 vtoclf.2 . . . . 5 𝐴 ∈ V
32isseti 3494 . . . 4 𝑥 𝑥 = 𝐴
4 vtoclf.3 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜓))
54biimpd 232 . . . 4 (𝑥 = 𝐴 → (𝜑𝜓))
63, 5eximii 1838 . . 3 𝑥(𝜑𝜓)
71, 619.36i 2235 . 2 (∀𝑥𝜑𝜓)
8 vtoclf.4 . 2 𝜑
97, 8mpg 1799 1 𝜓
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209   = wceq 1538  wnf 1785  wcel 2115  Vcvv 3480
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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-12 2179  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786  df-cleq 2817  df-clel 2896
This theorem is referenced by:  vtoclALT  3546  summolem2a  15068  prodmolem2a  15284  poimirlem24  34991  poimirlem28  34995  monotuz  39735  oddcomabszz  39738  binomcxplemnotnn0  40917  limclner  42156  climinf2mpt  42219  climinfmpt  42220  dvnmptdivc  42443  dvnmul  42448  salpreimagtge  43222  salpreimaltle  43223
  Copyright terms: Public domain W3C validator