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

Theorem vtocl2g 2849
Description: Implicit substitution of 2 classes for 2 set 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 2421 . 2  |-  F/_ x A
2 nfcv 2421 . 2  |-  F/_ y A
3 nfcv 2421 . 2  |-  F/_ y B
4 nfv 1607 . 2  |-  F/ x ps
5 nfv 1607 . 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 2847 1  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1625    e. wcel 1686
This theorem is referenced by:  ifexg  3626  uniprg  3844  intprg  3898  opthg  4248  opelopabsb  4277  unexb  4522  vtoclr  4735  elimasng  5041  cnvsng  5160  funopg  5288  f1osng  5516  fsng  5699  fvsng  5716  op1stg  6134  op2ndg  6135  xpsneng  6949  xpcomeng  6956  sbth  6983  unxpdom  7072  fpwwe2lem5  8258  prcdnq  8619  brimageg  24468  brdomaing  24476  brrangeg  24477  rankung  24798  pgapspf2  26064  zindbi  27042  2sbc6g  27626  2sbc5g  27627
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