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

Theorem vtoclgf 2954
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 2908 . 2  |-  ( A  e.  V  ->  A  e.  _V )
2 vtoclgf.1 . . . 4  |-  F/_ x A
32issetf 2905 . . 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 1811 . . 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 1717   F/_wnfc 2511   _Vcvv 2900
This theorem is referenced by:  vtoclg  2955  vtocl2gf  2957  vtocl3gf  2958  vtoclgaf  2960  ceqsexg  3011  elabgf  3024  mob  3060  opeliunxp2  4954  fvopab5  6471  cnextfvval  18018  dvfsumlem2  19779  dvfsumlem4  19781  ssiun2sf  23855  subtr  26009  subtr2  26010  fmul01  27379  fmuldfeqlem1  27381  fmuldfeq  27382  fmul01lt1lem1  27383  climsuse  27403  stoweidlem3  27421  stoweidlem26  27444  stoweidlem31  27449  stoweidlem43  27461  stoweidlem51  27469  stoweidlem59  27477
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 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-v 2902
  Copyright terms: Public domain W3C validator