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

Theorem vtoclgaf 2850
Description: Implicit substitution of a class for a set variable. (Contributed by NM, 17-Feb-2006.) (Revised by Mario Carneiro, 10-Oct-2016.)
Hypotheses
Ref Expression
vtoclgaf.1  |-  F/_ x A
vtoclgaf.2  |-  F/ x ps
vtoclgaf.3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
vtoclgaf.4  |-  ( x  e.  B  ->  ph )
Assertion
Ref Expression
vtoclgaf  |-  ( A  e.  B  ->  ps )
Distinct variable group:    x, B
Allowed substitution hints:    ph( x)    ps( x)    A( x)

Proof of Theorem vtoclgaf
StepHypRef Expression
1 vtoclgaf.1 . . 3  |-  F/_ x A
21nfel1 2431 . . . 4  |-  F/ x  A  e.  B
3 vtoclgaf.2 . . . 4  |-  F/ x ps
42, 3nfim 1771 . . 3  |-  F/ x
( A  e.  B  ->  ps )
5 eleq1 2345 . . . 4  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
6 vtoclgaf.3 . . . 4  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
75, 6imbi12d 311 . . 3  |-  ( x  =  A  ->  (
( x  e.  B  ->  ph )  <->  ( A  e.  B  ->  ps )
) )
8 vtoclgaf.4 . . 3  |-  ( x  e.  B  ->  ph )
91, 4, 7, 8vtoclgf 2844 . 2  |-  ( A  e.  B  ->  ( A  e.  B  ->  ps ) )
109pm2.43i 43 1  |-  ( A  e.  B  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   F/wnf 1533    = wceq 1625    e. wcel 1686   F/_wnfc 2408
This theorem is referenced by:  vtoclga  2851  ssiun2s  3948  tfis  4647  fvmptss  5611  fvmptf  5618  fmptco  5693  inar1  8399  sumss  12199  prmind2  12771  lss1d  15722  itg2splitlem  19105  dgrle  19627  cnlnadjlem5  22653  fmul01  27721  fmuldfeqlem1  27723  fmuldfeq  27724  fmul01lt1lem1  27725  fmul01lt1lem2  27726  climmulf  27741  climsuse  27745  climrecf  27746  stoweidlem3  27763  stoweidlem26  27786  stoweidlem30  27790  stoweidlem31  27791  stoweidlem34  27794  stoweidlem42  27802  stoweidlem43  27803  stoweidlem48  27808  stoweidlem62  27822  wallispi  27830
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-v 2792
  Copyright terms: Public domain W3C validator