Metamath Proof Explorer

Theorem dfrab2

Description: Alternate definition of restricted class abstraction. (Contributed by NM, 20-Sep-2003) (Proof shortened by BJ, 22-Apr-2019)

Ref Expression
Assertion dfrab2 
|- { x e. A | ph } = ( { x | ph } i^i A )

Proof

Step Hyp Ref Expression
1 dfrab3 
 |-  { x e. A | ph } = ( A i^i { x | ph } )
2 incom 
 |-  ( A i^i { x | ph } ) = ( { x | ph } i^i A )
3 1 2 eqtri 
 |-  { x e. A | ph } = ( { x | ph } i^i A )