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

Theorem vtoclgf 3104
Description: Implicit substitution of a class for a setvar variable, with bound-variable hypotheses in place of disjoint 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 3053 . 2  |-  ( A  e.  V  ->  A  e.  _V )
2 vtoclgf.1 . . . 4  |-  F/_ x A
32issetf 3049 . . 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 215 . . . 4  |-  ( x  =  A  ->  ps )
84, 7exlimi 1994 . . 3  |-  ( E. x  x  =  A  ->  ps )
93, 8sylbi 199 . 2  |-  ( A  e.  _V  ->  ps )
101, 9syl 17 1  |-  ( A  e.  V  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    = wceq 1443   E.wex 1662   F/wnf 1666    e. wcel 1886   F/_wnfc 2578   _Vcvv 3044
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-v 3046
This theorem is referenced by:  vtocl2gf  3108  vtocl3gf  3109  vtoclgaf  3111  elabgf  3182  fprodsplit1f  14037  ssiun2sf  28167  subtr  30963  subtr2  30964  supxrgere  37550  supxrgelem  37554  supxrge  37555  fsumsplit1  37645  fmuldfeqlem1  37654  climsuse  37681  dvnmptdivc  37807  dvmptfprodlem  37813  stoweidlem59  37914  fourierdlem31  37994  fourierdlem31OLD  37995  sge0f1o  38218  sge0fodjrnlem  38252
  Copyright terms: Public domain W3C validator