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 AVAx|φxφAx

Proof

Step Hyp Ref Expression
1 elintg AVAx|φyx|φAy
2 eleq2w y=xAyAx
3 2 ralab2 yx|φAyxφAx
4 1 3 bitrdi AVAx|φxφAx