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

Theorem vtoclgf 3464
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 3413 . 2 (𝐴𝑉𝐴 ∈ V)
2 vtoclgf.1 . . . 4 𝑥𝐴
32issetf 3409 . . 3 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
4 vtoclgf.2 . . . 4 𝑥𝜓
5 vtoclgf.4 . . . . 5 𝜑
6 vtoclgf.3 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜓))
75, 6mpbii 225 . . . 4 (𝑥 = 𝐴𝜓)
84, 7exlimi 2202 . . 3 (∃𝑥 𝑥 = 𝐴𝜓)
93, 8sylbi 209 . 2 (𝐴 ∈ V → 𝜓)
101, 9syl 17 1 (𝐴𝑉𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198   = wceq 1601  wex 1823  wnf 1827  wcel 2106  wnfc 2918  Vcvv 3397
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-ext 2753
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-v 3399
This theorem is referenced by:  vtocl2gf  3468  vtocl3gf  3469  vtoclgaf  3472  elabgf  3553  ssiun2sf  29940  subtr  32897  subtr2  32898  supxrgere  40439  supxrgelem  40443  supxrge  40444  fsumsplit1  40694  fmuldfeqlem1  40704  fprodcnlem  40721  climsuse  40730  dvnmptdivc  41063  dvmptfprodlem  41069  stoweidlem59  41185  fourierdlem31  41264  sge0f1o  41505  sge0fodjrnlem  41539  salpreimagelt  41827  salpreimalegt  41829
  Copyright terms: Public domain W3C validator