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

Theorem vtocl2g 2932
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 2502 . 2  |-  F/_ x A
2 nfcv 2502 . 2  |-  F/_ y A
3 nfcv 2502 . 2  |-  F/_ y B
4 nfv 1624 . 2  |-  F/ x ps
5 nfv 1624 . 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 2930 1  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1647    e. wcel 1715
This theorem is referenced by:  ifexg  3713  uniprg  3944  intprg  3998  opthg  4349  opelopabsb  4378  unexb  4623  vtoclr  4836  elimasng  5142  cnvsng  5261  funopg  5389  f1osng  5620  fsng  5808  fvsng  5827  op1stg  6259  op2ndg  6260  xpsneng  7090  xpcomeng  7097  sbth  7124  unxpdom  7213  fpwwe2lem5  8403  prcdnq  8764  brimageg  25207  brdomaing  25215  brrangeg  25216  rankung  25538  zindbi  26537  2sbc6g  27121  2sbc5g  27122  2pthoncl  27741
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-v 2875
  Copyright terms: Public domain W3C validator