Theorem rabeq0

Description: Condition for a restricted class abstraction to be empty. (Contributed by Jeff Madsen, 7-Jun-2010) (Revised by BJ, 16-Jul-2021)

	Ref	Expression
Assertion	rabeq0	|- ( { x e. A | ph } = (/) <-> A. x e. A -. ph )

Proof

Step	Hyp	Ref	Expression
1		ab0	|- ( { x | ( x e. A /\ ph ) } = (/) <-> A. x -. ( x e. A /\ ph ) )
2		df-rab	|- { x e. A | ph } = { x | ( x e. A /\ ph ) }
3	2	eqeq1i	|- ( { x e. A | ph } = (/) <-> { x | ( x e. A /\ ph ) } = (/) )
4		raln	|- ( A. x e. A -. ph <-> A. x -. ( x e. A /\ ph ) )
5	1 3 4	3bitr4i	|- ( { x e. A | ph } = (/) <-> A. x e. A -. ph )