This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ \{x \in A \| φ\} = \{x \| φ\} \cap A$

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