Theorem rabeqcOLD

Description: Obsolete version of rabeqc as of 15-Jan-2025. (Contributed by AV, 20-Apr-2022) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	rabeqcOLD.1	$$⊢x\in A\to \phi$$
Assertion	rabeqcOLD	$$⊢\left\{x\in A|\phi \right\}=A$$

Proof

Step	Hyp	Ref	Expression
1		rabeqcOLD.1	$$⊢x\in A\to \phi$$
2		df-rab	$$⊢\left\{x\in A|\phi \right\}=\left\{x|\left(x\in A\wedge \phi \right)\right\}$$
3		eqabcb	$$⊢\left\{x|\left(x\in A\wedge \phi \right)\right\}=A\leftrightarrow \forall x\left(\left(x\in A\wedge \phi \right)\leftrightarrow x\in A\right)$$
4	1	pm4.71i	$$⊢x\in A\leftrightarrow \left(x\in A\wedge \phi \right)$$
5	4	bicomi	$$⊢\left(x\in A\wedge \phi \right)\leftrightarrow x\in A$$
6	3 5	mpgbir	$$⊢\left\{x|\left(x\in A\wedge \phi \right)\right\}=A$$
7	2 6	eqtri	$$⊢\left\{x\in A|\phi \right\}=A$$