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

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

Proof

Step Hyp Ref Expression
1 vtocl3gf.a ⊢ Ⅎ 𝑥 𝐴
2 vtocl3gf.b ⊢ Ⅎ 𝑦 𝐴
3 vtocl3gf.c ⊢ Ⅎ 𝑧 𝐴
4 vtocl3gf.d ⊢ Ⅎ 𝑦 𝐵
5 vtocl3gf.e ⊢ Ⅎ 𝑧 𝐵
6 vtocl3gf.f ⊢ Ⅎ 𝑧 𝐶
7 vtocl3gf.1 ⊢ Ⅎ 𝑥 𝜓
8 vtocl3gf.2 ⊢ Ⅎ 𝑦 𝜒
9 vtocl3gf.3 ⊢ Ⅎ 𝑧 𝜃
10 vtocl3gf.4 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
11 vtocl3gf.5 ⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
12 vtocl3gf.6 ⊢ ( 𝑧 = 𝐶 → ( 𝜒 ↔ 𝜃 ) )
13 vtocl3gf.7 ⊢ 𝜑
14 elex ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
15 2 nfel1 ⊢ Ⅎ 𝑦 𝐴 ∈ V
16 15 8 nfim ⊢ Ⅎ 𝑦 ( 𝐴 ∈ V → 𝜒 )
17 3 nfel1 ⊢ Ⅎ 𝑧 𝐴 ∈ V
18 17 9 nfim ⊢ Ⅎ 𝑧 ( 𝐴 ∈ V → 𝜃 )
19 11 imbi2d ⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 ∈ V → 𝜓 ) ↔ ( 𝐴 ∈ V → 𝜒 ) ) )
20 12 imbi2d ⊢ ( 𝑧 = 𝐶 → ( ( 𝐴 ∈ V → 𝜒 ) ↔ ( 𝐴 ∈ V → 𝜃 ) ) )
21 1 7 10 13 vtoclgf ⊢ ( 𝐴 ∈ V → 𝜓 )
22 4 5 6 16 18 19 20 21 vtocl2gf ⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 ∈ V → 𝜃 ) )
23 14 22 mpan9 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ) → 𝜃 )
24 23 3impb ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → 𝜃 )