Theorem dfrab2

Description: Alternate definition of restricted class abstraction. (Contributed by NM, 20-Sep-2003) (Proof shortened by BJ, 22-Apr-2019)

	Ref	Expression
Assertion	dfrab2	$$⊢\left\{x\in A|\phi \right\}=\left\{x|\phi \right\}\cap A$$

Proof

Step	Hyp	Ref	Expression
1		dfrab3	$$⊢\left\{x\in A|\phi \right\}=A\cap \left\{x|\phi \right\}$$
2		incom	$$⊢A\cap \left\{x|\phi \right\}=\left\{x|\phi \right\}\cap A$$
3	1 2	eqtri	$$⊢\left\{x\in A|\phi \right\}=\left\{x|\phi \right\}\cap A$$