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	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → 𝜃 )