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 x A | φ x A φ


Step Hyp Ref Expression
1 df-rab x A | φ = x | x A φ
2 1 abeq2i x x A | φ x A φ