cgsexg

Description: Implicit substitution inference for general classes. (Contributed by NM, 26-Aug-2007)

	Ref	Expression
Hypotheses	cgsexg.1	$⊢ x = A \to χ$
	cgsexg.2	$⊢ χ \to (φ \leftrightarrow ψ)$
Assertion	cgsexg	$⊢ A \in V \to (\exists x (χ \land φ) \leftrightarrow ψ)$

Step	Hyp	Ref	Expression
1		cgsexg.1	$⊢ x = A \to χ$
2		cgsexg.2	$⊢ χ \to (φ \leftrightarrow ψ)$
3	2	biimpa	$⊢ (χ \land φ) \to ψ$
4	3	exlimiv	$⊢ \exists x (χ \land φ) \to ψ$
5		elisset	$⊢ A \in V \to \exists x x = A$
6	1	eximi	$⊢ \exists x x = A \to \exists x χ$
7	5 6	syl	$⊢ A \in V \to \exists x χ$
8	2	biimprcd	$⊢ ψ \to (χ \to φ)$
9	8	ancld	$⊢ ψ \to (χ \to (χ \land φ))$
10	9	eximdv	$⊢ ψ \to (\exists x χ \to \exists x (χ \land φ))$
11	7 10	syl5com	$⊢ A \in V \to (ψ \to \exists x (χ \land φ))$
12	4 11	impbid2	$⊢ A \in V \to (\exists x (χ \land φ) \leftrightarrow ψ)$

Metamath Proof Explorer