Metamath Proof Explorer

Theorem vtocl3gf

Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 10-Aug-2013) (Revised by Mario Carneiro, 10-Oct-2016)

Ref Expression
Hypotheses vtocl3gf.a ⊢ Ⅎ _ x A
vtocl3gf.b ⊢ Ⅎ _ y A
vtocl3gf.c ⊢ Ⅎ _ z A
vtocl3gf.d ⊢ Ⅎ _ y B
vtocl3gf.e ⊢ Ⅎ _ z B
vtocl3gf.f ⊢ Ⅎ _ z C
vtocl3gf.1 ⊢ Ⅎ x ψ
vtocl3gf.2 ⊢ Ⅎ y χ
vtocl3gf.3 ⊢ Ⅎ z θ
vtocl3gf.4 ⊢ x = A → φ ↔ ψ
vtocl3gf.5 ⊢ y = B → ψ ↔ χ
vtocl3gf.6 ⊢ z = C → χ ↔ θ
vtocl3gf.7 ⊢ φ
Assertion vtocl3gf ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ X → θ

Proof

Step Hyp Ref Expression
1 vtocl3gf.a ⊢ Ⅎ _ x A
2 vtocl3gf.b ⊢ Ⅎ _ y A
3 vtocl3gf.c ⊢ Ⅎ _ z A
4 vtocl3gf.d ⊢ Ⅎ _ y B
5 vtocl3gf.e ⊢ Ⅎ _ z B
6 vtocl3gf.f ⊢ Ⅎ _ z C
7 vtocl3gf.1 ⊢ Ⅎ x ψ
8 vtocl3gf.2 ⊢ Ⅎ y χ
9 vtocl3gf.3 ⊢ Ⅎ z θ
10 vtocl3gf.4 ⊢ x = A → φ ↔ ψ
11 vtocl3gf.5 ⊢ y = B → ψ ↔ χ
12 vtocl3gf.6 ⊢ z = C → χ ↔ θ
13 vtocl3gf.7 ⊢ φ
14 elex ⊢ A ∈ V → A ∈ V
15 2 nfel1 ⊢ Ⅎ y A ∈ V
16 15 8 nfim ⊢ Ⅎ y A ∈ V → χ
17 3 nfel1 ⊢ Ⅎ z A ∈ V
18 17 9 nfim ⊢ Ⅎ z A ∈ V → θ
19 11 imbi2d ⊢ y = B → A ∈ V → ψ ↔ A ∈ V → χ
20 12 imbi2d ⊢ z = C → A ∈ V → χ ↔ A ∈ V → θ
21 1 7 10 13 vtoclgf ⊢ A ∈ V → ψ
22 4 5 6 16 18 19 20 21 vtocl2gf ⊢ B ∈ W ∧ C ∈ X → A ∈ V → θ
23 14 22 mpan9 ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ X → θ
24 23 3impb ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ X → θ