Theorem rababg

Description: Condition when restricted class is equal to unrestricted class. (Contributed by RP, 13-Aug-2020)

	Ref	Expression
Assertion	rababg	$$⊢\forall x\left(\phi \to x\in A\right)\leftrightarrow \left\{x\in A|\phi \right\}=\left\{x|\phi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		ancrb	$$⊢\left(\phi \to x\in A\right)\leftrightarrow \left(\phi \to \left(x\in A\wedge \phi \right)\right)$$
2	1	albii	$$⊢\forall x\left(\phi \to x\in A\right)\leftrightarrow \forall x\left(\phi \to \left(x\in A\wedge \phi \right)\right)$$
3		nfv	$$⊢Ⅎy\left(\phi \to \left(x\in A\wedge \phi \right)\right)$$
4		nfsab1	$$⊢Ⅎxy\in \left\{x|\phi \right\}$$
5		nfrab1	$$⊢\underset{\_}{Ⅎ}x\left\{x\in A|\phi \right\}$$
6	5	nfcri	$$⊢Ⅎxy\in \left\{x\in A|\phi \right\}$$
7	4 6	nfim	$$⊢Ⅎx\left(y\in \left\{x|\phi \right\}\to y\in \left\{x\in A|\phi \right\}\right)$$
8		abid	$$⊢x\in \left\{x|\phi \right\}\leftrightarrow \phi$$
9		eleq1w	$$⊢x=y\to \left(x\in \left\{x|\phi \right\}\leftrightarrow y\in \left\{x|\phi \right\}\right)$$
10	8 9	bitr3id	$$⊢x=y\to \left(\phi \leftrightarrow y\in \left\{x|\phi \right\}\right)$$
11		rabid	$$⊢x\in \left\{x\in A|\phi \right\}\leftrightarrow \left(x\in A\wedge \phi \right)$$
12		eleq1w	$$⊢x=y\to \left(x\in \left\{x\in A|\phi \right\}\leftrightarrow y\in \left\{x\in A|\phi \right\}\right)$$
13	11 12	bitr3id	$$⊢x=y\to \left(\left(x\in A\wedge \phi \right)\leftrightarrow y\in \left\{x\in A|\phi \right\}\right)$$
14	10 13	imbi12d	$$⊢x=y\to \left(\left(\phi \to \left(x\in A\wedge \phi \right)\right)\leftrightarrow \left(y\in \left\{x|\phi \right\}\to y\in \left\{x\in A|\phi \right\}\right)\right)$$
15	3 7 14	cbvalv1	$$⊢\forall x\left(\phi \to \left(x\in A\wedge \phi \right)\right)\leftrightarrow \forall y\left(y\in \left\{x|\phi \right\}\to y\in \left\{x\in A|\phi \right\}\right)$$
16		eqss	$$⊢\left\{x\in A|\phi \right\}=\left\{x|\phi \right\}\leftrightarrow \left(\left\{x\in A|\phi \right\}\subseteq \left\{x|\phi \right\}\wedge \left\{x|\phi \right\}\subseteq \left\{x\in A|\phi \right\}\right)$$
17		rabssab	$$⊢\left\{x\in A|\phi \right\}\subseteq \left\{x|\phi \right\}$$
18	17	biantrur	$$⊢\left\{x|\phi \right\}\subseteq \left\{x\in A|\phi \right\}\leftrightarrow \left(\left\{x\in A|\phi \right\}\subseteq \left\{x|\phi \right\}\wedge \left\{x|\phi \right\}\subseteq \left\{x\in A|\phi \right\}\right)$$
19		dfss2	$$⊢\left\{x|\phi \right\}\subseteq \left\{x\in A|\phi \right\}\leftrightarrow \forall y\left(y\in \left\{x|\phi \right\}\to y\in \left\{x\in A|\phi \right\}\right)$$
20	16 18 19	3bitr2ri	$$⊢\forall y\left(y\in \left\{x|\phi \right\}\to y\in \left\{x\in A|\phi \right\}\right)\leftrightarrow \left\{x\in A|\phi \right\}=\left\{x|\phi \right\}$$
21	2 15 20	3bitri	$$⊢\forall x\left(\phi \to x\in A\right)\leftrightarrow \left\{x\in A|\phi \right\}=\left\{x|\phi \right\}$$