Theorem vtocl2g 2671

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

Step	Hyp	Ref	Expression
1		nfcv 2223	. 2 |- F/_ x A
2		nfcv 2223	. 2 |- F/_ y A
3		nfcv 2223	. 2 |- F/_ y B
4		nfv 1462	. 2 |- F/ x ps
5		nfv 1462	. 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 2669	1 |- ( ( A e. V /\ B e. W ) -> ch )

Syntax hints:   -> wi 4   /\ wa 102   <-> wb 103   = wceq 1285   e. wcel 1434

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065

This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-v 2612

This theorem is referenced by:  uniprg  3636  intprg  3689  opthg  4021  opelopabsb  4043  unexb  4223  vtoclr  4434  elimasng  4743  cnvsng  4856  funopg  4984  f1osng  5218  fsng  5388  fvsng  5411  op1stg  5828  op2ndg  5829  xpsneng  6387  xpcomeng  6393  bdunexb  10978  bj-unexg  10979