Theorem bj-ab0

Description: The class of sets verifying a falsity is the empty set (closed form of abf ). (Contributed by BJ, 24-Jul-2019) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-ab0	⊢ ( ∀ 𝑥 ¬ 𝜑 → { 𝑥 ∣ 𝜑 } = ∅ )

Proof

Step	Hyp	Ref	Expression
1		stdpc4	⊢ ( ∀ 𝑥 ¬ 𝜑 → [ 𝑦 / 𝑥 ] ¬ 𝜑 )
2		sbn1	⊢ ( [ 𝑦 / 𝑥 ] ¬ 𝜑 → ¬ [ 𝑦 / 𝑥 ] 𝜑 )
3	1 2	syl	⊢ ( ∀ 𝑥 ¬ 𝜑 → ¬ [ 𝑦 / 𝑥 ] 𝜑 )
4		df-clab	⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ [ 𝑦 / 𝑥 ] 𝜑 )
5	3 4	sylnibr	⊢ ( ∀ 𝑥 ¬ 𝜑 → ¬ 𝑦 ∈ { 𝑥 ∣ 𝜑 } )
6	5	eq0rdv	⊢ ( ∀ 𝑥 ¬ 𝜑 → { 𝑥 ∣ 𝜑 } = ∅ )