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	⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } = ∅ ↔ ∀ 𝑥 ∈ 𝐴 ¬ 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		ab0	⊢ ( { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } = ∅ ↔ ∀ 𝑥 ¬ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
2		df-rab	⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) }
3	2	eqeq1i	⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } = ∅ ↔ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } = ∅ )
4		raln	⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀ 𝑥 ¬ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
5	1 3 4	3bitr4i	⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } = ∅ ↔ ∀ 𝑥 ∈ 𝐴 ¬ 𝜑 )