Metamath Proof Explorer

Theorem vtocl2gaf

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

Ref Expression
Hypotheses vtocl2gaf.a ⊢ Ⅎ _ x A
vtocl2gaf.b ⊢ Ⅎ _ y A
vtocl2gaf.c ⊢ Ⅎ _ y B
vtocl2gaf.1 ⊢ Ⅎ x ψ
vtocl2gaf.2 ⊢ Ⅎ y χ
vtocl2gaf.3 ⊢ x = A → φ ↔ ψ
vtocl2gaf.4 ⊢ y = B → ψ ↔ χ
vtocl2gaf.5 ⊢ x ∈ C ∧ y ∈ D → φ
Assertion vtocl2gaf ⊢ A ∈ C ∧ B ∈ D → χ

Proof

Step Hyp Ref Expression
1 vtocl2gaf.a ⊢ Ⅎ _ x A
2 vtocl2gaf.b ⊢ Ⅎ _ y A
3 vtocl2gaf.c ⊢ Ⅎ _ y B
4 vtocl2gaf.1 ⊢ Ⅎ x ψ
5 vtocl2gaf.2 ⊢ Ⅎ y χ
6 vtocl2gaf.3 ⊢ x = A → φ ↔ ψ
7 vtocl2gaf.4 ⊢ y = B → ψ ↔ χ
8 vtocl2gaf.5 ⊢ x ∈ C ∧ y ∈ D → φ
9 1 nfel1 ⊢ Ⅎ x A ∈ C
10 nfv ⊢ Ⅎ x y ∈ D
11 9 10 nfan ⊢ Ⅎ x A ∈ C ∧ y ∈ D
12 11 4 nfim ⊢ Ⅎ x A ∈ C ∧ y ∈ D → ψ
13 2 nfel1 ⊢ Ⅎ y A ∈ C
14 3 nfel1 ⊢ Ⅎ y B ∈ D
15 13 14 nfan ⊢ Ⅎ y A ∈ C ∧ B ∈ D
16 15 5 nfim ⊢ Ⅎ y A ∈ C ∧ B ∈ D → χ
17 eleq1 ⊢ x = A → x ∈ C ↔ A ∈ C
18 17 anbi1d ⊢ x = A → x ∈ C ∧ y ∈ D ↔ A ∈ C ∧ y ∈ D
19 18 6 imbi12d ⊢ x = A → x ∈ C ∧ y ∈ D → φ ↔ A ∈ C ∧ y ∈ D → ψ
20 eleq1 ⊢ y = B → y ∈ D ↔ B ∈ D
21 20 anbi2d ⊢ y = B → A ∈ C ∧ y ∈ D ↔ A ∈ C ∧ B ∈ D
22 21 7 imbi12d ⊢ y = B → A ∈ C ∧ y ∈ D → ψ ↔ A ∈ C ∧ B ∈ D → χ
23 1 2 3 12 16 19 22 8 vtocl2gf ⊢ A ∈ C ∧ B ∈ D → A ∈ C ∧ B ∈ D → χ
24 23 pm2.43i ⊢ A ∈ C ∧ B ∈ D → χ