Theorem vtocl2gaf

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

	Ref	Expression
Hypotheses	vtocl2gaf.a	⊢ Ⅎ 𝑥 𝐴
	vtocl2gaf.b	⊢ Ⅎ 𝑦 𝐴
	vtocl2gaf.c	⊢ Ⅎ 𝑦 𝐵
	vtocl2gaf.1	⊢ Ⅎ 𝑥 𝜓
	vtocl2gaf.2	⊢ Ⅎ 𝑦 𝜒
	vtocl2gaf.3	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
	vtocl2gaf.4	⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
	vtocl2gaf.5	⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) → 𝜑 )
Assertion	vtocl2gaf	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → 𝜒 )

Proof

Step	Hyp	Ref	Expression
1		vtocl2gaf.a	⊢ Ⅎ 𝑥 𝐴
2		vtocl2gaf.b	⊢ Ⅎ 𝑦 𝐴
3		vtocl2gaf.c	⊢ Ⅎ 𝑦 𝐵
4		vtocl2gaf.1	⊢ Ⅎ 𝑥 𝜓
5		vtocl2gaf.2	⊢ Ⅎ 𝑦 𝜒
6		vtocl2gaf.3	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
7		vtocl2gaf.4	⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
8		vtocl2gaf.5	⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) → 𝜑 )
9	1	nfel1	⊢ Ⅎ 𝑥 𝐴 ∈ 𝐶
10		nfv	⊢ Ⅎ 𝑥 𝑦 ∈ 𝐷
11	9 10	nfan	⊢ Ⅎ 𝑥 ( 𝐴 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 )
12	11 4	nfim	⊢ Ⅎ 𝑥 ( ( 𝐴 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) → 𝜓 )
13	2	nfel1	⊢ Ⅎ 𝑦 𝐴 ∈ 𝐶
14	3	nfel1	⊢ Ⅎ 𝑦 𝐵 ∈ 𝐷
15	13 14	nfan	⊢ Ⅎ 𝑦 ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 )
16	15 5	nfim	⊢ Ⅎ 𝑦 ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → 𝜒 )
17		eleq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶 ) )
18	17	anbi1d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ↔ ( 𝐴 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ) )
19	18 6	imbi12d	⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) → 𝜑 ) ↔ ( ( 𝐴 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) → 𝜓 ) ) )
20		eleq1	⊢ ( 𝑦 = 𝐵 → ( 𝑦 ∈ 𝐷 ↔ 𝐵 ∈ 𝐷 ) )
21	20	anbi2d	⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ↔ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) ) )
22	21 7	imbi12d	⊢ ( 𝑦 = 𝐵 → ( ( ( 𝐴 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) → 𝜓 ) ↔ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → 𝜒 ) ) )
23	1 2 3 12 16 19 22 8	vtocl2gf	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → 𝜒 ) )
24	23	pm2.43i	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → 𝜒 )