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

Theorem vtoclgf 2855
Description: Implicit substitution of a class for a set variable, with bound-variable hypotheses in place of distinct 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 2809 . 2  |-  ( A  e.  V  ->  A  e.  _V )
2 vtoclgf.1 . . . 4  |-  F/_ x A
32issetf 2806 . . 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 202 . . . 4  |-  ( x  =  A  ->  ps )
84, 7exlimi 1813 . . 3  |-  ( E. x  x  =  A  ->  ps )
93, 8sylbi 187 . 2  |-  ( A  e.  _V  ->  ps )
101, 9syl 15 1  |-  ( A  e.  V  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   E.wex 1531   F/wnf 1534    = wceq 1632    e. wcel 1696   F/_wnfc 2419   _Vcvv 2801
This theorem is referenced by:  vtoclg  2856  vtocl2gf  2858  vtocl3gf  2859  vtoclgaf  2861  ceqsexg  2912  elabgf  2925  mob  2960  opeliunxp2  4840  fvopab5  6305  dvfsumlem2  19390  dvfsumlem4  19392  ssiun2sf  23173  fmptcof2  23244  subtr  26327  subtr2  26328  stoweidlem51  27903  stoweidlem59  27911
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803
  Copyright terms: Public domain W3C validator