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 z = y z x y x
3 2 imbi2d z = y x B z x x B y x
4 3 albidv z = y x x B z x x x B y x
5 eleq1 y = A y x A x
6 5 imbi2d y = A x B y x x B A x
7 6 albidv y = A x x B y x x x B A x
8 df-int B = z | x x B z x
9 4 7 8 elab2gw A V A B x x B A x
10 1 9 ax-mp A B x x B A x