Theorem vtocl2g 3017

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

Step	Hyp	Ref	Expression
1		nfcv 2574	. 2 |- F/_ x A
2		nfcv 2574	. 2 |- F/_ y A
3		nfcv 2574	. 2 |- F/_ y B
4		nfv 1630	. 2 |- F/ x ps
5		nfv 1630	. 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
9	1, 2, 3, 4, 5, 6, 7, 8	vtocl2gf 3015	1 |- ( ( A e. V /\ B e. W ) -> ch )

Syntax hints:   -> wi 4   <-> wb 178   /\ wa 360   = wceq 1653   e. wcel 1726

This theorem is referenced by:  ifexg  3800  uniprg  4032  intprg  4086  opthg  4439  opelopabsb  4468  unexb  4712  vtoclr  4925  elimasng  5233  cnvsng  5358  funopg  5488  f1osng  5719  fsng  5910  fvsng  5930  op1stg  6362  op2ndg  6363  xpsneng  7196  xpcomeng  7203  sbth  7230  unxpdom  7319  fpwwe2lem5  8514  prcdnq  8875  2pthoncl  21608  brimageg  25777  brdomaing  25785  brrangeg  25786  rankung  26112  mbfresfi  26265  zindbi  27023  2sbc6g  27606  2sbc5g  27607  fmulcl  27701

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419

This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960