Metamath Proof Explorer


Theorem elint

Description: Membership in class intersection. (Contributed by NM, 21-May-1994)

Ref Expression
Hypothesis elint.1
|- A e. _V
Assertion elint
|- ( A e. |^| B <-> A. x ( x e. B -> A e. x ) )

Proof

Step Hyp Ref Expression
1 elint.1
 |-  A e. _V
2 eleq1
 |-  ( y = A -> ( y e. x <-> A e. x ) )
3 2 imbi2d
 |-  ( y = A -> ( ( x e. B -> y e. x ) <-> ( x e. B -> A e. x ) ) )
4 3 albidv
 |-  ( y = A -> ( A. x ( x e. B -> y e. x ) <-> A. x ( x e. B -> A e. x ) ) )
5 df-int
 |-  |^| B = { y | A. x ( x e. B -> y e. x ) }
6 4 5 elab2g
 |-  ( A e. _V -> ( A e. |^| B <-> A. x ( x e. B -> A e. x ) ) )
7 1 6 ax-mp
 |-  ( A e. |^| B <-> A. x ( x e. B -> A e. x ) )