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	$⊢ x = A \to (φ \leftrightarrow ψ)$
	vtocl2g.2	$⊢ y = B \to (ψ \leftrightarrow χ)$
	vtocl2g.3	$⊢ φ$
Assertion	vtocl2g	$⊢ (A \in V \land B \in W) \to χ$

Proof

Step	Hyp	Ref	Expression
1		vtocl2g.1	$⊢ x = A \to (φ \leftrightarrow ψ)$
2		vtocl2g.2	$⊢ y = B \to (ψ \leftrightarrow χ)$
3		vtocl2g.3	$⊢ φ$
4		elex	$⊢ A \in V \to A \in V$
5	2	imbi2d	$⊢ y = B \to ((A \in V \to ψ) \leftrightarrow (A \in V \to χ))$
6	1 3	vtoclg	$⊢ A \in V \to ψ$
7	5 6	vtoclg	$⊢ B \in W \to (A \in V \to χ)$
8	4 7	mpan9	$⊢ (A \in V \land B \in W) \to χ$