Theorem cgsexg

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

	Ref	Expression
Hypotheses	cgsexg.1	$$⊢x=A\to \chi$$
	cgsexg.2	$$⊢\chi \to \left(\phi \leftrightarrow \psi \right)$$
Assertion	cgsexg	$$⊢A\in V\to \left(\exists x\left(\chi \wedge \phi \right)\leftrightarrow \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		cgsexg.1	$$⊢x=A\to \chi$$
2		cgsexg.2	$$⊢\chi \to \left(\phi \leftrightarrow \psi \right)$$
3	2	biimpa	$$⊢\left(\chi \wedge \phi \right)\to \psi$$
4	3	exlimiv	$$⊢\exists x\left(\chi \wedge \phi \right)\to \psi$$
5		elisset	$$⊢A\in V\to \exists xx=A$$
6	1	eximi	$$⊢\exists xx=A\to \exists x\chi$$
7	5 6	syl	$$⊢A\in V\to \exists x\chi$$
8	2	biimprcd	$$⊢\psi \to \left(\chi \to \phi \right)$$
9	8	ancld	$$⊢\psi \to \left(\chi \to \left(\chi \wedge \phi \right)\right)$$
10	9	eximdv	$$⊢\psi \to \left(\exists x\chi \to \exists x\left(\chi \wedge \phi \right)\right)$$
11	7 10	syl5com	$$⊢A\in V\to \left(\psi \to \exists x\left(\chi \wedge \phi \right)\right)$$
12	4 11	impbid2	$$⊢A\in V\to \left(\exists x\left(\chi \wedge \phi \right)\leftrightarrow \psi \right)$$