Theorem vtocl2gaf 2922

Description: Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 10-Aug-2013.)

Hypotheses

Ref	Expression
vtocl2gaf.a	|- F/_xA
vtocl2gaf.b	|- F/_yA
vtocl2gaf.c	|- F/_yB
vtocl2gaf.1	|- F/xps
vtocl2gaf.2	|- F/ych
vtocl2gaf.3	|- (x = A -> (ph <-> ps))
vtocl2gaf.4	|- (y = B -> (ps <-> ch))
vtocl2gaf.5	|- ((x e. C /\ y e. D) -> ph)

Assertion

Ref	Expression
vtocl2gaf	|- ((A e. C /\ B e. D) -> ch)

Distinct variable groups:   x,y,C   x,D,y

Allowed substitution hints:   ph(x,y)   ps(x,y)   ch(x,y)   A(x,y)   B(x,y)

Proof of Theorem vtocl2gaf

Step	Hyp	Ref	Expression
1		vtocl2gaf.a	. . 3 |- F/_xA
2		vtocl2gaf.b	. . 3 |- F/_yA
3		vtocl2gaf.c	. . 3 |- F/_yB
4	1	nfel1 2500	. . . . 5 |- F/x A e. C
5		nfv 1619	. . . . 5 |- F/x y e. D
6	4, 5	nfan 1824	. . . 4 |- F/x(A e. C /\ y e. D)
7		vtocl2gaf.1	. . . 4 |- F/xps
8	6, 7	nfim 1813	. . 3 |- F/x((A e. C /\ y e. D) -> ps)
9	2	nfel1 2500	. . . . 5 |- F/y A e. C
10	3	nfel1 2500	. . . . 5 |- F/y B e. D
11	9, 10	nfan 1824	. . . 4 |- F/y(A e. C /\ B e. D)
12		vtocl2gaf.2	. . . 4 |- F/ych
13	11, 12	nfim 1813	. . 3 |- F/y((A e. C /\ B e. D) -> ch)
14		eleq1 2413	. . . . 5 |- (x = A -> (x e. C <-> A e. C))
15	14	anbi1d 685	. . . 4 |- (x = A -> ((x e. C /\ y e. D) <-> (A e. C /\ y e. D)))
16		vtocl2gaf.3	. . . 4 |- (x = A -> (ph <-> ps))
17	15, 16	imbi12d 311	. . 3 |- (x = A -> (((x e. C /\ y e. D) -> ph) <-> ((A e. C /\ y e. D) -> ps)))
18		eleq1 2413	. . . . 5 |- (y = B -> (y e. D <-> B e. D))
19	18	anbi2d 684	. . . 4 |- (y = B -> ((A e. C /\ y e. D) <-> (A e. C /\ B e. D)))
20		vtocl2gaf.4	. . . 4 |- (y = B -> (ps <-> ch))
21	19, 20	imbi12d 311	. . 3 |- (y = B -> (((A e. C /\ y e. D) -> ps) <-> ((A e. C /\ B e. D) -> ch)))
22		vtocl2gaf.5	. . 3 |- ((x e. C /\ y e. D) -> ph)
23	1, 2, 3, 8, 13, 17, 21, 22	vtocl2gf 2917	. 2 |- ((A e. C /\ B e. D) -> ((A e. C /\ B e. D) -> ch))
24	23	pm2.43i 43	1 |- ((A e. C /\ B e. D) -> ch)

Syntax hints:   -> wi 4   <-> wb 176   /\ wa 358   F/wnf 1544   = wceq 1642   e. wcel 1710   F/_wnfc 2477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-v 2862

This theorem is referenced by:  vtocl2ga  2923  ov3  5600  ov2gf  5712