Metamath Proof Explorer


Theorem elintab

Description: Membership in the intersection of a class abstraction. (Contributed by NM, 30-Aug-1993)

Ref Expression
Hypothesis inteqab.1 A V
Assertion elintab A x | φ x φ A x

Proof

Step Hyp Ref Expression
1 inteqab.1 A V
2 1 elint A x | φ y y x | φ A y
3 nfsab1 x y x | φ
4 nfv x A y
5 3 4 nfim x y x | φ A y
6 nfv y φ A x
7 eleq1w y = x y x | φ x x | φ
8 abid x x | φ φ
9 7 8 bitrdi y = x y x | φ φ
10 eleq2w y = x A y A x
11 9 10 imbi12d y = x y x | φ A y φ A x
12 5 6 11 cbvalv1 y y x | φ A y x φ A x
13 2 12 bitri A x | φ x φ A x