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

Metamath Proof Explorer

Theorem gencl

Description: Implicit substitution for class with embedded variable. (Contributed by NM, 17-May-1996)

	Ref	Expression
Hypotheses	gencl.1	$⊢ θ \leftrightarrow \exists x (χ \land A = B)$
	gencl.2	$⊢ A = B \to (φ \leftrightarrow ψ)$
	gencl.3	$⊢ χ \to φ$
Assertion	gencl	$⊢ θ \to ψ$

Step	Hyp	Ref	Expression
1		gencl.1	$⊢ θ \leftrightarrow \exists x (χ \land A = B)$
2		gencl.2	$⊢ A = B \to (φ \leftrightarrow ψ)$
3		gencl.3	$⊢ χ \to φ$
4	3 2	imbitrid	$⊢ A = B \to (χ \to ψ)$
5	4	impcom	$⊢ (χ \land A = B) \to ψ$
6	5	exlimiv	$⊢ \exists x (χ \land A = B) \to ψ$
7	1 6	sylbi	$⊢ θ \to ψ$