Metamath Proof Explorer

Theorem ssabral

Description: The relation for a subclass of a class abstraction is equivalent to restricted quantification. (Contributed by NM, 6-Sep-2006)

Ref Expression
Assertion ssabral A x | φ x A φ


Step Hyp Ref Expression
1 ssab A x | φ x x A φ
2 df-ral x A φ x x A φ
3 1 2 bitr4i A x | φ x A φ