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

Metamath Proof Explorer

Theorem vtocl2g

Description: Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 25-Apr-1995) Remove dependency on ax-10 , ax-11 , and ax-13 . (Revised by Steven Nguyen, 29-Nov-2022)

	Ref	Expression
Hypotheses	vtocl2g.1	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
	vtocl2g.2	⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
	vtocl2g.3	⊢ 𝜑
Assertion	vtocl2g	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝜒 )

Proof

Step	Hyp	Ref	Expression
1		vtocl2g.1	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
2		vtocl2g.2	⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
3		vtocl2g.3	⊢ 𝜑
4		elex	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
5	2	imbi2d	⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 ∈ V → 𝜓 ) ↔ ( 𝐴 ∈ V → 𝜒 ) ) )
6	1 3	vtoclg	⊢ ( 𝐴 ∈ V → 𝜓 )
7	5 6	vtoclg	⊢ ( 𝐵 ∈ 𝑊 → ( 𝐴 ∈ V → 𝜒 ) )
8	4 7	mpan9	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝜒 )