Metamath Proof Explorer


Theorem elint2

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

Ref Expression
Hypothesis elint2.1 AV
Assertion elint2 ABxBAx

Proof

Step Hyp Ref Expression
1 elint2.1 AV
2 1 elint ABxxBAx
3 df-ral xBAxxxBAx
4 2 3 bitr4i ABxBAx