Metamath Proof Explorer

Theorem dfint2

Description: Alternate definition of class intersection. (Contributed by NM, 28-Jun-1998)

Ref Expression
Assertion dfint2 
|- |^| A = { x | A. y e. A x e. y }

Proof

Step Hyp Ref Expression
1 df-int 
 |-  |^| A = { x | A. y ( y e. A -> x e. y ) }
2 df-ral 
 |-  ( A. y e. A x e. y <-> A. y ( y e. A -> x e. y ) )
3 2 abbii 
 |-  { x | A. y e. A x e. y } = { x | A. y ( y e. A -> x e. y ) }
4 1 3 eqtr4i 
 |-  |^| A = { x | A. y e. A x e. y }