This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ Ⅎ 𝑥 𝐴
vtocl3gaf.b ⊢ Ⅎ 𝑦 𝐴
vtocl3gaf.c ⊢ Ⅎ 𝑧 𝐴
vtocl3gaf.d ⊢ Ⅎ 𝑦 𝐵
vtocl3gaf.e ⊢ Ⅎ 𝑧 𝐵
vtocl3gaf.f ⊢ Ⅎ 𝑧 𝐶
vtocl3gaf.1 ⊢ Ⅎ 𝑥 𝜓
vtocl3gaf.2 ⊢ Ⅎ 𝑦 𝜒
vtocl3gaf.3 ⊢ Ⅎ 𝑧 𝜃
vtocl3gaf.4 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
vtocl3gaf.5 ⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
vtocl3gaf.6 ⊢ ( 𝑧 = 𝐶 → ( 𝜒 ↔ 𝜃 ) )
vtocl3gaf.7 ⊢ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇 ) → 𝜑 )
Assertion vtocl3gaf ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) → 𝜃 )

Proof

Step Hyp Ref Expression
1 vtocl3gaf.a ⊢ Ⅎ 𝑥 𝐴
2 vtocl3gaf.b ⊢ Ⅎ 𝑦 𝐴
3 vtocl3gaf.c ⊢ Ⅎ 𝑧 𝐴
4 vtocl3gaf.d ⊢ Ⅎ 𝑦 𝐵
5 vtocl3gaf.e ⊢ Ⅎ 𝑧 𝐵
6 vtocl3gaf.f ⊢ Ⅎ 𝑧 𝐶
7 vtocl3gaf.1 ⊢ Ⅎ 𝑥 𝜓
8 vtocl3gaf.2 ⊢ Ⅎ 𝑦 𝜒
9 vtocl3gaf.3 ⊢ Ⅎ 𝑧 𝜃
10 vtocl3gaf.4 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
11 vtocl3gaf.5 ⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
12 vtocl3gaf.6 ⊢ ( 𝑧 = 𝐶 → ( 𝜒 ↔ 𝜃 ) )
13 vtocl3gaf.7 ⊢ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇 ) → 𝜑 )
14 3 nfel1 ⊢ Ⅎ 𝑧 𝐴 ∈ 𝑅
15 5 nfel1 ⊢ Ⅎ 𝑧 𝐵 ∈ 𝑆
16 14 15 nfan ⊢ Ⅎ 𝑧 ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 )
17 16 9 nfim ⊢ Ⅎ 𝑧 ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) → 𝜃 )
18 12 imbi2d ⊢ ( 𝑧 = 𝐶 → ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) → 𝜒 ) ↔ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) → 𝜃 ) ) )
19 nfv ⊢ Ⅎ 𝑥 𝑧 ∈ 𝑇
20 19 7 nfim ⊢ Ⅎ 𝑥 ( 𝑧 ∈ 𝑇 → 𝜓 )
21 nfv ⊢ Ⅎ 𝑦 𝑧 ∈ 𝑇
22 21 8 nfim ⊢ Ⅎ 𝑦 ( 𝑧 ∈ 𝑇 → 𝜒 )
23 10 imbi2d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑧 ∈ 𝑇 → 𝜑 ) ↔ ( 𝑧 ∈ 𝑇 → 𝜓 ) ) )
24 11 imbi2d ⊢ ( 𝑦 = 𝐵 → ( ( 𝑧 ∈ 𝑇 → 𝜓 ) ↔ ( 𝑧 ∈ 𝑇 → 𝜒 ) ) )
25 13 3expia ⊢ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) → ( 𝑧 ∈ 𝑇 → 𝜑 ) )
26 1 2 4 20 22 23 24 25 vtocl2gaf ⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) → ( 𝑧 ∈ 𝑇 → 𝜒 ) )
27 26 com12 ⊢ ( 𝑧 ∈ 𝑇 → ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) → 𝜒 ) )
28 6 17 18 27 vtoclgaf ⊢ ( 𝐶 ∈ 𝑇 → ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) → 𝜃 ) )
29 28 impcom ⊢ ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝐶 ∈ 𝑇 ) → 𝜃 )
30 29 3impa ⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) → 𝜃 )