Metamath Proof Explorer


Theorem elintrab

Description: Membership in the intersection of a class abstraction. (Contributed by NM, 17-Oct-1999)

Ref Expression
Hypothesis inteqab.1 AV
Assertion elintrab AxB|φxBφAx

Proof

Step Hyp Ref Expression
1 inteqab.1 AV
2 1 elintab Ax|xBφxxBφAx
3 impexp xBφAxxBφAx
4 3 albii xxBφAxxxBφAx
5 2 4 bitri Ax|xBφxxBφAx
6 df-rab xB|φ=x|xBφ
7 6 inteqi xB|φ=x|xBφ
8 7 eleq2i AxB|φAx|xBφ
9 df-ral xBφAxxxBφAx
10 5 8 9 3bitr4i AxB|φxBφAx