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

Theorem vtoclgf 3002
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 2956 . 2  |-  ( A  e.  V  ->  A  e.  _V )
2 vtoclgf.1 . . . 4  |-  F/_ x A
32issetf 2953 . . 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 1821 . . 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 1550   F/wnf 1553    = wceq 1652    e. wcel 1725   F/_wnfc 2558   _Vcvv 2948
This theorem is referenced by:  vtoclg  3003  vtocl2gf  3005  vtocl3gf  3006  vtoclgaf  3008  ceqsexg  3059  elabgf  3072  mob  3108  opeliunxp2  5005  fvopab5  6526  cnextfvval  18086  dvfsumlem2  19901  dvfsumlem4  19903  ssiun2sf  24000  subtr  26271  subtr2  26272  fmul01  27641  fmuldfeqlem1  27643  fmuldfeq  27644  fmul01lt1lem1  27645  climsuse  27665  stoweidlem3  27683  stoweidlem26  27706  stoweidlem31  27711  stoweidlem43  27723  stoweidlem51  27731  stoweidlem59  27739
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950
  Copyright terms: Public domain W3C validator