Theorem rabid2f

Description: An "identity" law for restricted class abstraction. (Contributed by NM, 9-Oct-2003) (Proof shortened by Andrew Salmon, 30-May-2011) (Revised by Thierry Arnoux, 13-Mar-2017)

	Ref	Expression
Hypothesis	rabid2f.1	$$⊢\underset{\_}{Ⅎ}xA$$
Assertion	rabid2f	$$⊢A=\left\{x\in A|\phi \right\}\leftrightarrow \forall x\in A\phi$$

Proof

Step	Hyp	Ref	Expression
1		rabid2f.1	$$⊢\underset{\_}{Ⅎ}xA$$
2	1	abeq2f	$$⊢A=\left\{x|\left(x\in A\wedge \phi \right)\right\}\leftrightarrow \forall x\left(x\in A\leftrightarrow \left(x\in A\wedge \phi \right)\right)$$
3		pm4.71	$$⊢\left(x\in A\to \phi \right)\leftrightarrow \left(x\in A\leftrightarrow \left(x\in A\wedge \phi \right)\right)$$
4	3	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)$$
5	2 4	bitr4i	$$⊢A=\left\{x|\left(x\in A\wedge \phi \right)\right\}\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		df-ral	$$⊢\forall x\in A\phi \leftrightarrow \forall x\left(x\in A\to \phi \right)$$
9	5 7 8	3bitr4i	$$⊢A=\left\{x\in A|\phi \right\}\leftrightarrow \forall x\in A\phi$$