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 } |
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 } |