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

Theorem vtoclgf 2970
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 2924 . 2  |-  ( A  e.  V  ->  A  e.  _V )
2 vtoclgf.1 . . . 4  |-  F/_ x A
32issetf 2921 . . 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 203 . . . 4  |-  ( x  =  A  ->  ps )
84, 7exlimi 1817 . . 3  |-  ( E. x  x  =  A  ->  ps )
93, 8sylbi 188 . 2  |-  ( A  e.  _V  ->  ps )
101, 9syl 16 1  |-  ( A  e.  V  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   E.wex 1547   F/wnf 1550    = wceq 1649    e. wcel 1721   F/_wnfc 2527   _Vcvv 2916
This theorem is referenced by:  vtoclg  2971  vtocl2gf  2973  vtocl3gf  2974  vtoclgaf  2976  ceqsexg  3027  elabgf  3040  mob  3076  opeliunxp2  4972  fvopab5  6493  cnextfvval  18049  dvfsumlem2  19864  dvfsumlem4  19866  ssiun2sf  23963  subtr  26207  subtr2  26208  fmul01  27577  fmuldfeqlem1  27579  fmuldfeq  27580  fmul01lt1lem1  27581  climsuse  27601  stoweidlem3  27619  stoweidlem26  27642  stoweidlem31  27647  stoweidlem43  27659  stoweidlem51  27667  stoweidlem59  27675
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918
  Copyright terms: Public domain W3C validator