Theorem intexrab

Description: The intersection of a nonempty restricted class abstraction exists. (Contributed by NM, 21-Oct-2003)

	Ref	Expression
Assertion	intexrab	|- ( E. x e. A ph <-> |^| { x e. A | ph } e. _V )

Proof

Step	Hyp	Ref	Expression
1		intexab	|- ( E. x ( x e. A /\ ph ) <-> |^| { x | ( x e. A /\ ph ) } e. _V )
2		df-rex	|- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
3		df-rab	|- { x e. A | ph } = { x | ( x e. A /\ ph ) }
4	3	inteqi	|- |^| { x e. A | ph } = |^| { x | ( x e. A /\ ph ) }
5	4	eleq1i	|- ( |^| { x e. A | ph } e. _V <-> |^| { x | ( x e. A /\ ph ) } e. _V )
6	1 2 5	3bitr4i	|- ( E. x e. A ph <-> |^| { x e. A | ph } e. _V )