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

Theorem vtocl2g 3157
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 2605 . 2  |-  F/_ x A
2 nfcv 2605 . 2  |-  F/_ y A
3 nfcv 2605 . 2  |-  F/_ y B
4 nfv 1694 . 2  |-  F/ x ps
5 nfv 1694 . 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 3155 1  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1383    e. wcel 1804
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097
This theorem is referenced by:  vtocl4g  3164  ifexg  3996  uniprg  4248  intprg  4306  opthg  4712  opelopabsb  4747  vtoclr  5034  elimasng  5353  cnvsng  5484  funopg  5610  f1osng  5844  fsng  6055  fvsng  6090  unexb  6585  op1stg  6797  op2ndg  6798  xpsneng  7604  xpcomeng  7611  sbth  7639  unxpdom  7729  fpwwe2lem5  9015  prcdnq  9374  mhmlem  16169  2pthoncl  24583  brimageg  29553  brdomaing  29561  brrangeg  29562  rankung  29799  mbfresfi  30037  zindbi  30858  2sbc6g  31276  2sbc5g  31277  fmulcl  31529
  Copyright terms: Public domain W3C validator