Theorem rabid2im

Description: One direction of rabid2 is based on fewer axioms. (Contributed by Wolf Lammen, 26-May-2025)

	Ref	Expression
Assertion	rabid2im	$$⊢\forall x\in A\phi \to A=\left\{x\in A|\phi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		pm4.71	$$⊢\left(x\in A\to \phi \right)\leftrightarrow \left(x\in A\leftrightarrow \left(x\in A\wedge \phi \right)\right)$$
2	1	albii	$$⊢\forall x\left(x\in A\to \phi \right)\leftrightarrow \forall x\left(x\in A\leftrightarrow \left(x\in A\wedge \phi \right)\right)$$
3		eqab	$$⊢\forall x\left(x\in A\leftrightarrow \left(x\in A\wedge \phi \right)\right)\to A=\left\{x|\left(x\in A\wedge \phi \right)\right\}$$
4	2 3	sylbi	$$⊢\forall x\left(x\in A\to \phi \right)\to A=\left\{x|\left(x\in A\wedge \phi \right)\right\}$$
5		df-ral	$$⊢\forall x\in A\phi \leftrightarrow \forall x\left(x\in A\to \phi \right)$$
6		df-rab	$$⊢\left\{x\in A|\phi \right\}=\left\{x|\left(x\in A\wedge \phi \right)\right\}$$
7	6	eqeq2i	$$⊢A=\left\{x\in A|\phi \right\}\leftrightarrow A=\left\{x|\left(x\in A\wedge \phi \right)\right\}$$
8	4 5 7	3imtr4i	$$⊢\forall x\in A\phi \to A=\left\{x\in A|\phi \right\}$$