Metamath Proof Explorer


Theorem elintabg

Description: Two ways of saying a set is an element of the intersection of a class. (Contributed by RP, 13-Aug-2020)

Ref Expression
Assertion elintabg A V A x | φ x φ A x

Proof

Step Hyp Ref Expression
1 elintg A V A x | φ y x | φ A y
2 eleq2w y = x A y A x
3 2 ralab2 y x | φ A y x φ A x
4 1 3 bitrdi A V A x | φ x φ A x