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

Theorem vtoclgaf 2882
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 2462 . . . 4  |-  F/ x  A  e.  B
3 vtoclgaf.2 . . . 4  |-  F/ x ps
42, 3nfim 1792 . . 3  |-  F/ x
( A  e.  B  ->  ps )
5 eleq1 2376 . . . 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 2876 . 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 1535    = wceq 1633    e. wcel 1701   F/_wnfc 2439
This theorem is referenced by:  vtoclga  2883  ssiun2s  3983  tfis  4682  fvmptss  5647  fvmptf  5654  fmptco  5729  inar1  8442  sumss  12244  prmind2  12816  lss1d  15769  itg2splitlem  19156  dgrle  19678  cnlnadjlem5  22706  fmul01  26858  fmuldfeqlem1  26860  fmuldfeq  26861  fmul01lt1lem1  26862  fmul01lt1lem2  26863  climmulf  26878  climsuse  26882  climrecf  26883  stoweidlem3  26900  stoweidlem26  26923  stoweidlem30  26927  stoweidlem31  26928  stoweidlem34  26931  stoweidlem42  26939  stoweidlem43  26940  stoweidlem48  26945  stoweidlem62  26959  wallispi  26967
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-v 2824
  Copyright terms: Public domain W3C validator