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 eqabri 
 |-  ( x e. { x e. A | ph } <-> ( x e. A /\ ph ) )