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

Theorem vtoclgf 3416
Description: Implicit substitution of a class for a setvar variable, with bound-variable hypotheses in place of disjoint variable restrictions. (Contributed by NM, 21-Sep-2003.) (Proof shortened by Mario Carneiro, 10-Oct-2016.)
Hypotheses
Ref Expression
vtoclgf.1 𝑥𝐴
vtoclgf.2 𝑥𝜓
vtoclgf.3 (𝑥 = 𝐴 → (𝜑𝜓))
vtoclgf.4 𝜑
Assertion
Ref Expression
vtoclgf (𝐴𝑉𝜓)

Proof of Theorem vtoclgf
StepHypRef Expression
1 elex 3364 . 2 (𝐴𝑉𝐴 ∈ V)
2 vtoclgf.1 . . . 4 𝑥𝐴
32issetf 3360 . . 3 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
4 vtoclgf.2 . . . 4 𝑥𝜓
5 vtoclgf.4 . . . . 5 𝜑
6 vtoclgf.3 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜓))
75, 6mpbii 223 . . . 4 (𝑥 = 𝐴𝜓)
84, 7exlimi 2242 . . 3 (∃𝑥 𝑥 = 𝐴𝜓)
93, 8sylbi 207 . 2 (𝐴 ∈ V → 𝜓)
101, 9syl 17 1 (𝐴𝑉𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1631  wex 1852  wnf 1856  wcel 2145  wnfc 2900  Vcvv 3351
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353
This theorem is referenced by:  vtocl2gf  3420  vtocl3gf  3421  vtoclgaf  3423  elabgf  3500  fprodsplit1f  14928  ssiun2sf  29717  subtr  32646  subtr2  32647  supxrgere  40066  supxrgelem  40070  supxrge  40071  fsumsplit1  40323  fmuldfeqlem1  40333  fprodcnlem  40350  climsuse  40359  dvnmptdivc  40672  dvmptfprodlem  40678  stoweidlem59  40794  fourierdlem31  40873  sge0f1o  41117  sge0fodjrnlem  41151  salpreimagelt  41439  salpreimalegt  41441
  Copyright terms: Public domain W3C validator