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

Theorem vtoclgf 2842
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 2796 . 2  |-  ( A  e.  V  ->  A  e.  _V )
2 vtoclgf.1 . . . 4  |-  F/_ x A
32issetf 2793 . . 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 1801 . . 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 1528   F/wnf 1531    = wceq 1623    e. wcel 1684   F/_wnfc 2406   _Vcvv 2788
This theorem is referenced by:  vtoclg  2843  vtocl2gf  2845  vtocl3gf  2846  vtoclgaf  2848  ceqsexg  2899  elabgf  2912  mob  2947  opeliunxp2  4824  fvopab5  6289  dvfsumlem2  19374  dvfsumlem4  19376  subtr  25636  subtr2  25637  stoweidlem51  27212  stoweidlem59  27220
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790
  Copyright terms: Public domain W3C validator