Theorem rabeqc

Description: A restricted class abstraction equals the restricting class if its condition follows from the membership of the free setvar variable in the restricting class. (Contributed by AV, 20-Apr-2022)

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

Proof

Step	Hyp	Ref	Expression
1		rabeqc.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		abeq1	$$⊢\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$$