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

Metamath Proof Explorer

Theorem dfrab3

Description: Alternate definition of restricted class abstraction. (Contributed by Mario Carneiro, 8-Sep-2013)

		Ref	Expression
	Assertion	dfrab3	$⊢ \{x \in A \| φ\} = A \cap \{x \| φ\}$

Step	Hyp	Ref	Expression
1		df-rab	$⊢ \{x \in A \| φ\} = \{x \| (x \in A \land φ)\}$
2		inab	$⊢ \{x \| x \in A\} \cap \{x \| φ\} = \{x \| (x \in A \land φ)\}$
3		abid2	$⊢ \{x \| x \in A\} = A$
4	3	ineq1i	$⊢ \{x \| x \in A\} \cap \{x \| φ\} = A \cap \{x \| φ\}$
5	1 2 4	3eqtr2i	$⊢ \{x \in A \| φ\} = A \cap \{x \| φ\}$