Theorem vtocl2gaf 2921

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

Hypotheses

Ref	Expression
vtocl2gaf.a	⊢ ℲxA
vtocl2gaf.b	⊢ ℲyA
vtocl2gaf.c	⊢ ℲyB
vtocl2gaf.1	⊢ Ⅎxψ
vtocl2gaf.2	⊢ Ⅎyχ
vtocl2gaf.3	⊢ (x = A → (φ ↔ ψ))
vtocl2gaf.4	⊢ (y = B → (ψ ↔ χ))
vtocl2gaf.5	⊢ ((x ∈ C ∧ y ∈ D) → φ)

Assertion

Ref	Expression
vtocl2gaf	⊢ ((A ∈ C ∧ B ∈ D) → χ)

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

Allowed substitution hints:   φ(x,y)   ψ(x,y)   χ(x,y)   A(x,y)   B(x,y)

Proof of Theorem vtocl2gaf

Step	Hyp	Ref	Expression
1		vtocl2gaf.a	. . 3 ⊢ ℲxA
2		vtocl2gaf.b	. . 3 ⊢ ℲyA
3		vtocl2gaf.c	. . 3 ⊢ ℲyB
4	1	nfel1 2499	. . . . 5 ⊢ Ⅎx A ∈ C
5		nfv 1619	. . . . 5 ⊢ Ⅎx y ∈ D
6	4, 5	nfan 1824	. . . 4 ⊢ Ⅎx(A ∈ C ∧ y ∈ D)
7		vtocl2gaf.1	. . . 4 ⊢ Ⅎxψ
8	6, 7	nfim 1813	. . 3 ⊢ Ⅎx((A ∈ C ∧ y ∈ D) → ψ)
9	2	nfel1 2499	. . . . 5 ⊢ Ⅎy A ∈ C
10	3	nfel1 2499	. . . . 5 ⊢ Ⅎy B ∈ D
11	9, 10	nfan 1824	. . . 4 ⊢ Ⅎy(A ∈ C ∧ B ∈ D)
12		vtocl2gaf.2	. . . 4 ⊢ Ⅎyχ
13	11, 12	nfim 1813	. . 3 ⊢ Ⅎy((A ∈ C ∧ B ∈ D) → χ)
14		eleq1 2413	. . . . 5 ⊢ (x = A → (x ∈ C ↔ A ∈ C))
15	14	anbi1d 685	. . . 4 ⊢ (x = A → ((x ∈ C ∧ y ∈ D) ↔ (A ∈ C ∧ y ∈ D)))
16		vtocl2gaf.3	. . . 4 ⊢ (x = A → (φ ↔ ψ))
17	15, 16	imbi12d 311	. . 3 ⊢ (x = A → (((x ∈ C ∧ y ∈ D) → φ) ↔ ((A ∈ C ∧ y ∈ D) → ψ)))
18		eleq1 2413	. . . . 5 ⊢ (y = B → (y ∈ D ↔ B ∈ D))
19	18	anbi2d 684	. . . 4 ⊢ (y = B → ((A ∈ C ∧ y ∈ D) ↔ (A ∈ C ∧ B ∈ D)))
20		vtocl2gaf.4	. . . 4 ⊢ (y = B → (ψ ↔ χ))
21	19, 20	imbi12d 311	. . 3 ⊢ (y = B → (((A ∈ C ∧ y ∈ D) → ψ) ↔ ((A ∈ C ∧ B ∈ D) → χ)))
22		vtocl2gaf.5	. . 3 ⊢ ((x ∈ C ∧ y ∈ D) → φ)
23	1, 2, 3, 8, 13, 17, 21, 22	vtocl2gf 2916	. 2 ⊢ ((A ∈ C ∧ B ∈ D) → ((A ∈ C ∧ B ∈ D) → χ))
24	23	pm2.43i 43	1 ⊢ ((A ∈ C ∧ B ∈ D) → χ)

Syntax hints:   → wi 4   ↔ wb 176   ∧ wa 358  Ⅎwnf 1544   = wceq 1642   ∈ wcel 1710  Ⅎwnfc 2476

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 2478  df-v 2861

This theorem is referenced by:  vtocl2ga  2922  ov3  5599  ov2gf  5711