Theorem elrabi

Description: Implication for the membership in a restricted class abstraction. (Contributed by Alexander van der Vekens, 31-Dec-2017) Remove disjoint variable condition on A , x and avoid ax-10 , ax-11 , ax-12 . (Revised by SN, 5-Aug-2024)

	Ref	Expression
Assertion	elrabi	$$⊢A\in \left\{x\in V|\phi \right\}\to A\in V$$

Proof

Step	Hyp	Ref	Expression
1		dfclel	$$⊢A\in \left\{x|\left(x\in V\wedge \phi \right)\right\}\leftrightarrow \exists y\left(y=A\wedge y\in \left\{x|\left(x\in V\wedge \phi \right)\right\}\right)$$
2		df-clab	$$⊢y\in \left\{x|\left(x\in V\wedge \phi \right)\right\}\leftrightarrow \left[y/x\right]\left(x\in V\wedge \phi \right)$$
3		simpl	$$⊢\left(x\in V\wedge \phi \right)\to x\in V$$
4	3	sbimi	$$⊢\left[y/x\right]\left(x\in V\wedge \phi \right)\to \left[y/x\right]x\in V$$
5		clelsb1	$$⊢\left[y/x\right]x\in V\leftrightarrow y\in V$$
6	4 5	sylib	$$⊢\left[y/x\right]\left(x\in V\wedge \phi \right)\to y\in V$$
7	2 6	sylbi	$$⊢y\in \left\{x|\left(x\in V\wedge \phi \right)\right\}\to y\in V$$
8		eleq1	$$⊢y=A\to \left(y\in V\leftrightarrow A\in V\right)$$
9	8	biimpa	$$⊢\left(y=A\wedge y\in V\right)\to A\in V$$
10	7 9	sylan2	$$⊢\left(y=A\wedge y\in \left\{x|\left(x\in V\wedge \phi \right)\right\}\right)\to A\in V$$
11	10	exlimiv	$$⊢\exists y\left(y=A\wedge y\in \left\{x|\left(x\in V\wedge \phi \right)\right\}\right)\to A\in V$$
12	1 11	sylbi	$$⊢A\in \left\{x|\left(x\in V\wedge \phi \right)\right\}\to A\in V$$
13		df-rab	$$⊢\left\{x\in V|\phi \right\}=\left\{x|\left(x\in V\wedge \phi \right)\right\}$$
14	12 13	eleq2s	$$⊢A\in \left\{x\in V|\phi \right\}\to A\in V$$