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 }