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

Theorem vtocl2g 3175
Description: Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 25-Apr-1995.)
Hypotheses
Ref Expression
vtocl2g.1  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
vtocl2g.2  |-  ( y  =  B  ->  ( ps 
<->  ch ) )
vtocl2g.3  |-  ph
Assertion
Ref Expression
vtocl2g  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ch )
Distinct variable groups:    x, A    y, A    y, B    ps, x    ch, y
Allowed substitution hints:    ph( x, y)    ps( y)    ch( x)    B( x)    V( x, y)    W( x, y)

Proof of Theorem vtocl2g
StepHypRef Expression
1 nfcv 2629 . 2  |-  F/_ x A
2 nfcv 2629 . 2  |-  F/_ y A
3 nfcv 2629 . 2  |-  F/_ y B
4 nfv 1683 . 2  |-  F/ x ps
5 nfv 1683 . 2  |-  F/ y ch
6 vtocl2g.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
7 vtocl2g.2 . 2  |-  ( y  =  B  ->  ( ps 
<->  ch ) )
8 vtocl2g.3 . 2  |-  ph
91, 2, 3, 4, 5, 6, 7, 8vtocl2gf 3173 1  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1379    e. wcel 1767
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115
This theorem is referenced by:  vtocl4g  3182  ifexg  4009  uniprg  4259  intprg  4316  opthg  4722  opelopabsb  4757  vtoclr  5044  elimasng  5363  cnvsng  5494  funopg  5620  f1osng  5854  fsng  6060  fvsng  6095  unexb  6584  op1stg  6796  op2ndg  6797  xpsneng  7602  xpcomeng  7609  sbth  7637  unxpdom  7727  fpwwe2lem5  9012  prcdnq  9371  2pthoncl  24309  brimageg  29182  brdomaing  29190  brrangeg  29191  rankung  29428  mbfresfi  29666  zindbi  30514  2sbc6g  30928  2sbc5g  30929  fmulcl  31159
  Copyright terms: Public domain W3C validator