Theorem elab3gf

Description: Membership in a class abstraction, with a weaker antecedent than elabgf . (Contributed by NM, 6-Sep-2011)

	Ref	Expression
Hypotheses	elab3gf.1	$$⊢\underset{\_}{Ⅎ}xA$$
	elab3gf.2	$$⊢Ⅎx\psi$$
	elab3gf.3	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	elab3gf	$$⊢\left(\psi \to A\in B\right)\to \left(A\in \left\{x|\phi \right\}\leftrightarrow \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		elab3gf.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		elab3gf.2	$$⊢Ⅎx\psi$$
3		elab3gf.3	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
4	1 2 3	elabgf	$$⊢A\in \left\{x|\phi \right\}\to \left(A\in \left\{x|\phi \right\}\leftrightarrow \psi \right)$$
5	4	ibi	$$⊢A\in \left\{x|\phi \right\}\to \psi$$
6		pm2.21	$$⊢\neg \psi \to \left(\psi \to A\in \left\{x|\phi \right\}\right)$$
7	5 6	impbid2	$$⊢\neg \psi \to \left(A\in \left\{x|\phi \right\}\leftrightarrow \psi \right)$$
8	1 2 3	elabgf	$$⊢A\in B\to \left(A\in \left\{x|\phi \right\}\leftrightarrow \psi \right)$$
9	7 8	ja	$$⊢\left(\psi \to A\in B\right)\to \left(A\in \left\{x|\phi \right\}\leftrightarrow \psi \right)$$