cgsex2g

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

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

Step	Hyp	Ref	Expression
1		cgsex2g.1	$⊢ (x = A \land y = B) \to χ$
2		cgsex2g.2	$⊢ χ \to (φ \leftrightarrow ψ)$
3	2	biimpa	$⊢ (χ \land φ) \to ψ$
4	3	exlimivv	$⊢ \exists x \exists y (χ \land φ) \to ψ$
5		elisset	$⊢ A \in V \to \exists x x = A$
6		elisset	$⊢ B \in W \to \exists y y = B$
7	5 6	anim12i	$⊢ (A \in V \land B \in W) \to (\exists x x = A \land \exists y y = B)$
8		exdistrv	$⊢ \exists x \exists y (x = A \land y = B) \leftrightarrow (\exists x x = A \land \exists y y = B)$
9	7 8	sylibr	$⊢ (A \in V \land B \in W) \to \exists x \exists y (x = A \land y = B)$
10	1	2eximi	$⊢ \exists x \exists y (x = A \land y = B) \to \exists x \exists y χ$
11	9 10	syl	$⊢ (A \in V \land B \in W) \to \exists x \exists y χ$
12	2	biimprcd	$⊢ ψ \to (χ \to φ)$
13	12	ancld	$⊢ ψ \to (χ \to (χ \land φ))$
14	13	2eximdv	$⊢ ψ \to (\exists x \exists y χ \to \exists x \exists y (χ \land φ))$
15	11 14	syl5com	$⊢ (A \in V \land B \in W) \to (ψ \to \exists x \exists y (χ \land φ))$
16	4 15	impbid2	$⊢ (A \in V \land B \in W) \to (\exists x \exists y (χ \land φ) \leftrightarrow ψ)$

Metamath Proof Explorer