Metamath Proof Explorer


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 ) )