Theorem rabid

Description: An "identity" law of concretion for restricted abstraction. Special case of Definition 2.1 of Quine p. 16. (Contributed by NM, 9-Oct-2003)

	Ref	Expression
Assertion	rabid	|- ( x e. { x e. A | ph } <-> ( x e. A /\ ph ) )

Proof

Step	Hyp	Ref	Expression
1		df-rab	|- { x e. A | ph } = { x | ( x e. A /\ ph ) }
2	1	abeq2i	|- ( x e. { x e. A | ph } <-> ( x e. A /\ ph ) )