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

Theorem vtoclgf 3165
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  |-  F/_ x A
vtoclgf.2  |-  F/ x ps
vtoclgf.3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
vtoclgf.4  |-  ph
Assertion
Ref Expression
vtoclgf  |-  ( A  e.  V  ->  ps )

Proof of Theorem vtoclgf
StepHypRef Expression
1 elex 3118 . 2  |-  ( A  e.  V  ->  A  e.  _V )
2 vtoclgf.1 . . . 4  |-  F/_ x A
32issetf 3114 . . 3  |-  ( A  e.  _V  <->  E. x  x  =  A )
4 vtoclgf.2 . . . 4  |-  F/ x ps
5 vtoclgf.4 . . . . 5  |-  ph
6 vtoclgf.3 . . . . 5  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
75, 6mpbii 211 . . . 4  |-  ( x  =  A  ->  ps )
84, 7exlimi 1913 . . 3  |-  ( E. x  x  =  A  ->  ps )
93, 8sylbi 195 . 2  |-  ( A  e.  _V  ->  ps )
101, 9syl 16 1  |-  ( A  e.  V  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1395   E.wex 1613   F/wnf 1617    e. wcel 1819   F/_wnfc 2605   _Vcvv 3109
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111
This theorem is referenced by:  vtocl2gf  3169  vtocl3gf  3170  vtoclgaf  3172  elabgf  3244  ssiun2sf  27565  subtr  30337  subtr2  30338  fsumsplit1  31776  fmuldfeqlem1  31779  fprodsplit1f  31796  climsuse  31817  dvnmptdivc  31938  dvmptfprodlem  31944  stoweidlem59  32044  fourierdlem31  32123
  Copyright terms: Public domain W3C validator