Metamath Proof Explorer

Theorem vtocl3gaf

Description: Implicit substitution of 3 classes for 3 setvar variables. (Contributed by NM, 10-Aug-2013) (Revised by Mario Carneiro, 11-Oct-2016) (Proof shortened by Wolf Lammen, 31-May-2025)

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

Proof

Step Hyp Ref Expression
1 vtocl3gaf.a ⊢ Ⅎ _ x A
2 vtocl3gaf.b ⊢ Ⅎ _ y A
3 vtocl3gaf.c ⊢ Ⅎ _ z A
4 vtocl3gaf.d ⊢ Ⅎ _ y B
5 vtocl3gaf.e ⊢ Ⅎ _ z B
6 vtocl3gaf.f ⊢ Ⅎ _ z C
7 vtocl3gaf.1 ⊢ Ⅎ x ψ
8 vtocl3gaf.2 ⊢ Ⅎ y χ
9 vtocl3gaf.3 ⊢ Ⅎ z θ
10 vtocl3gaf.4 ⊢ x = A → φ ↔ ψ
11 vtocl3gaf.5 ⊢ y = B → ψ ↔ χ
12 vtocl3gaf.6 ⊢ z = C → χ ↔ θ
13 vtocl3gaf.7 ⊢ x ∈ R ∧ y ∈ S ∧ z ∈ T → φ
14 3 nfel1 ⊢ Ⅎ z A ∈ R
15 5 nfel1 ⊢ Ⅎ z B ∈ S
16 14 15 nfan ⊢ Ⅎ z A ∈ R ∧ B ∈ S
17 16 9 nfim ⊢ Ⅎ z A ∈ R ∧ B ∈ S → θ
18 12 imbi2d ⊢ z = C → A ∈ R ∧ B ∈ S → χ ↔ A ∈ R ∧ B ∈ S → θ
19 nfv ⊢ Ⅎ x z ∈ T
20 19 7 nfim ⊢ Ⅎ x z ∈ T → ψ
21 nfv ⊢ Ⅎ y z ∈ T
22 21 8 nfim ⊢ Ⅎ y z ∈ T → χ
23 10 imbi2d ⊢ x = A → z ∈ T → φ ↔ z ∈ T → ψ
24 11 imbi2d ⊢ y = B → z ∈ T → ψ ↔ z ∈ T → χ
25 13 3expia ⊢ x ∈ R ∧ y ∈ S → z ∈ T → φ
26 1 2 4 20 22 23 24 25 vtocl2gaf ⊢ A ∈ R ∧ B ∈ S → z ∈ T → χ
27 26 com12 ⊢ z ∈ T → A ∈ R ∧ B ∈ S → χ
28 6 17 18 27 vtoclgaf ⊢ C ∈ T → A ∈ R ∧ B ∈ S → θ
29 28 impcom ⊢ A ∈ R ∧ B ∈ S ∧ C ∈ T → θ
30 29 3impa ⊢ A ∈ R ∧ B ∈ S ∧ C ∈ T → θ