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

Theorem vtoclf 3407
Description: Implicit substitution of a class for a setvar variable. This is a generalization of chvar 2423. (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 3358 . . . 4 𝑥 𝑥 = 𝐴
4 vtoclf.3 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜓))
54biimpd 219 . . . 4 (𝑥 = 𝐴 → (𝜑𝜓))
63, 5eximii 1911 . . 3 𝑥(𝜑𝜓)
71, 619.36i 2254 . 2 (∀𝑥𝜑𝜓)
8 vtoclf.4 . 2 𝜑
97, 8mpg 1871 1 𝜓
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1630  wnf 1855  wcel 2144  Vcvv 3349
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-12 2202  ax-ext 2750
This theorem depends on definitions:  df-bi 197  df-an 383  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-v 3351
This theorem is referenced by:  vtoclALT  3409  summolem2a  14653  prodmolem2a  14870  poimirlem24  33759  poimirlem28  33763  monotuz  38025  oddcomabszz  38028  binomcxplemnotnn0  39074  limclner  40395  climinf2mpt  40458  climinfmpt  40459  dvnmptdivc  40665  dvnmul  40670  salpreimagtge  41448  salpreimaltle  41449
  Copyright terms: Public domain W3C validator