Theorem elab3g

Description: Membership in a class abstraction, with a weaker antecedent than elabg . (Contributed by NM, 29-Aug-2006)

	Ref	Expression
Hypothesis	elab3g.1	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	elab3g	$$⊢\left(\psi \to A\in B\right)\to \left(A\in \left\{x|\phi \right\}\leftrightarrow \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		elab3g.1	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
2	1	elabg	$$⊢A\in \left\{x|\phi \right\}\to \left(A\in \left\{x|\phi \right\}\leftrightarrow \psi \right)$$
3	2	ibi	$$⊢A\in \left\{x|\phi \right\}\to \psi$$
4		pm2.21	$$⊢\neg \psi \to \left(\psi \to A\in \left\{x|\phi \right\}\right)$$
5	3 4	impbid2	$$⊢\neg \psi \to \left(A\in \left\{x|\phi \right\}\leftrightarrow \psi \right)$$
6	1	elabg	$$⊢A\in B\to \left(A\in \left\{x|\phi \right\}\leftrightarrow \psi \right)$$
7	5 6	ja	$$⊢\left(\psi \to A\in B\right)\to \left(A\in \left\{x|\phi \right\}\leftrightarrow \psi \right)$$