Theorem vtocl2gf

Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 25-Apr-1995)

	Ref	Expression
Hypotheses	vtocl2gf.1	⊢ Ⅎ 𝑥 𝐴
	vtocl2gf.2	⊢ Ⅎ 𝑦 𝐴
	vtocl2gf.3	⊢ Ⅎ 𝑦 𝐵
	vtocl2gf.4	⊢ Ⅎ 𝑥 𝜓
	vtocl2gf.5	⊢ Ⅎ 𝑦 𝜒
	vtocl2gf.6	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
	vtocl2gf.7	⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
	vtocl2gf.8	⊢ 𝜑
Assertion	vtocl2gf	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝜒 )

Proof

Step	Hyp	Ref	Expression
1		vtocl2gf.1	⊢ Ⅎ 𝑥 𝐴
2		vtocl2gf.2	⊢ Ⅎ 𝑦 𝐴
3		vtocl2gf.3	⊢ Ⅎ 𝑦 𝐵
4		vtocl2gf.4	⊢ Ⅎ 𝑥 𝜓
5		vtocl2gf.5	⊢ Ⅎ 𝑦 𝜒
6		vtocl2gf.6	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
7		vtocl2gf.7	⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
8		vtocl2gf.8	⊢ 𝜑
9		elex	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
10	2	nfel1	⊢ Ⅎ 𝑦 𝐴 ∈ V
11	10 5	nfim	⊢ Ⅎ 𝑦 ( 𝐴 ∈ V → 𝜒 )
12	7	imbi2d	⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 ∈ V → 𝜓 ) ↔ ( 𝐴 ∈ V → 𝜒 ) ) )
13	1 4 6 8	vtoclgf	⊢ ( 𝐴 ∈ V → 𝜓 )
14	3 11 12 13	vtoclgf	⊢ ( 𝐵 ∈ 𝑊 → ( 𝐴 ∈ V → 𝜒 ) )
15	9 14	mpan9	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝜒 )