Metamath Proof Explorer


Theorem elint

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

Ref Expression
Hypothesis elint.1 A V
Assertion elint A B x x B A x

Proof

Step Hyp Ref Expression
1 elint.1 A V
2 eleq1 y = A y x A x
3 2 imbi2d y = A x B y x x B A x
4 3 albidv y = A x x B y x x x B A x
5 df-int B = y | x x B y x
6 1 4 5 elab2 A B x x B A x