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

Theorem vtoclf 3253
Description: Implicit substitution of a class for a setvar variable. This is a generalization of chvar 2260. (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 3204 . . . 4 𝑥 𝑥 = 𝐴
4 vtoclf.3 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜓))
54biimpd 219 . . . 4 (𝑥 = 𝐴 → (𝜑𝜓))
63, 5eximii 1762 . . 3 𝑥(𝜑𝜓)
71, 619.36i 2097 . 2 (∀𝑥𝜑𝜓)
8 vtoclf.4 . 2 𝜑
97, 8mpg 1722 1 𝜓
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1481  wnf 1706  wcel 1988  Vcvv 3195
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-12 2045  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-v 3197
This theorem is referenced by:  vtoclALT  3255  summolem2a  14427  prodmolem2a  14645  poimirlem24  33404  poimirlem28  33408  monotuz  37325  oddcomabszz  37328  binomcxplemnotnn0  38375  limclner  39683  climinf2mpt  39746  climinfmpt  39747  dvnmptdivc  39916  dvnmul  39921  salpreimagtge  40697  salpreimaltle  40698
  Copyright terms: Public domain W3C validator