Metamath Proof Explorer


Theorem elint2

Description: Membership in class intersection. (Contributed by NM, 14-Oct-1999)

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

Proof

Step Hyp Ref Expression
1 elint2.1 A V
2 1 elint A B x x B A x
3 df-ral x B A x x x B A x
4 2 3 bitr4i A B x B A x