Theorem vtocl2g 2983

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 2548	. 2 |- F/_ x A
2		nfcv 2548	. 2 |- F/_ y A
3		nfcv 2548	. 2 |- F/_ y B
4		nfv 1626	. 2 |- F/ x ps
5		nfv 1626	. 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 2981	1 |- ( ( A e. V /\ B e. W ) -> ch )

Syntax hints:   -> wi 4   <-> wb 177   /\ wa 359   = wceq 1649   e. wcel 1721

This theorem is referenced by:  ifexg  3766  uniprg  3998  intprg  4052  opthg  4404  opelopabsb  4433  unexb  4676  vtoclr  4889  elimasng  5197  cnvsng  5322  funopg  5452  f1osng  5683  fsng  5874  fvsng  5894  op1stg  6326  op2ndg  6327  xpsneng  7160  xpcomeng  7167  sbth  7194  unxpdom  7283  fpwwe2lem5  8473  prcdnq  8834  2pthoncl  21564  brimageg  25688  brdomaing  25696  brrangeg  25697  rankung  26019  mbfresfi  26160  zindbi  26907  2sbc6g  27491  2sbc5g  27492  fmulcl  27586

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-v 2926