Theorem elssabg

Description: Membership in a class abstraction involving a subset. Unlike elabg , A does not have to be a set. (Contributed by NM, 29-Aug-2006)

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

Proof

Step	Hyp	Ref	Expression
1		elssabg.1	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
2		ssexg	$$⊢\left(A\subseteq B\wedge B\in V\right)\to A\in \mathrm{V}$$
3	2	expcom	$$⊢B\in V\to \left(A\subseteq B\to A\in \mathrm{V}\right)$$
4	3	adantrd	$$⊢B\in V\to \left(\left(A\subseteq B\wedge \psi \right)\to A\in \mathrm{V}\right)$$
5		sseq1	$$⊢x=A\to \left(x\subseteq B\leftrightarrow A\subseteq B\right)$$
6	5 1	anbi12d	$$⊢x=A\to \left(\left(x\subseteq B\wedge \phi \right)\leftrightarrow \left(A\subseteq B\wedge \psi \right)\right)$$
7	6	elab3g	$$⊢\left(\left(A\subseteq B\wedge \psi \right)\to A\in \mathrm{V}\right)\to \left(A\in \left\{x|\left(x\subseteq B\wedge \phi \right)\right\}\leftrightarrow \left(A\subseteq B\wedge \psi \right)\right)$$
8	4 7	syl	$$⊢B\in V\to \left(A\in \left\{x|\left(x\subseteq B\wedge \phi \right)\right\}\leftrightarrow \left(A\subseteq B\wedge \psi \right)\right)$$