Metamath Proof Explorer


Theorem elintd

Description: Membership in class intersection. (Contributed by Glauco Siliprandi, 3-Jan-2021)

Ref Expression
Hypotheses elintd.1 x φ
elintd.2 φ A V
elintd.3 φ x B A x
Assertion elintd φ A B

Proof

Step Hyp Ref Expression
1 elintd.1 x φ
2 elintd.2 φ A V
3 elintd.3 φ x B A x
4 3 ex φ x B A x
5 1 4 ralrimi φ x B A x
6 elintg A V A B x B A x
7 2 6 syl φ A B x B A x
8 5 7 mpbird φ A B