Theorem elintabg

Description: Two ways of saying a set is an element of the intersection of a class. (Contributed by NM, 30-Aug-1993) Put in closed form. (Revised by RP, 13-Aug-2020)

	Ref	Expression
Assertion	elintabg	|- ( A e. V -> ( A e. |^| { x | ph } <-> A. x ( ph -> A e. x ) ) )

Proof

Step	Hyp	Ref	Expression
1		elintg	|- ( A e. V -> ( A e. |^| { x | ph } <-> A. y e. { x | ph } A e. y ) )
2		eleq2w	|- ( y = x -> ( A e. y <-> A e. x ) )
3	2	ralab2	|- ( A. y e. { x | ph } A e. y <-> A. x ( ph -> A e. x ) )
4	1 3	bitrdi	|- ( A e. V -> ( A e. |^| { x | ph } <-> A. x ( ph -> A e. x ) ) )