Theorem ab0w

Description: The class of sets verifying a property is the empty class if and only if that property is a contradiction. Version of ab0 using implicit substitution, which requires fewer axioms. (Contributed by GG, 3-Oct-2024)

	Ref	Expression
Hypothesis	ab0w.1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
Assertion	ab0w	⊢ ( { 𝑥 ∣ 𝜑 } = ∅ ↔ ∀ 𝑦 ¬ 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		ab0w.1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2		dfnul4	⊢ ∅ = { 𝑥 ∣ ⊥ }
3	2	eqeq2i	⊢ ( { 𝑥 ∣ 𝜑 } = ∅ ↔ { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ ⊥ } )
4		dfcleq	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ ⊥ } ↔ ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝑦 ∈ { 𝑥 ∣ ⊥ } ) )
5		df-clab	⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ [ 𝑦 / 𝑥 ] 𝜑 )
6	1	sbievw	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 )
7	5 6	bitri	⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜓 )
8	7	bibi1i	⊢ ( ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝑦 ∈ { 𝑥 ∣ ⊥ } ) ↔ ( 𝜓 ↔ 𝑦 ∈ { 𝑥 ∣ ⊥ } ) )
9		bicom	⊢ ( ( 𝜓 ↔ 𝑦 ∈ { 𝑥 ∣ ⊥ } ) ↔ ( 𝑦 ∈ { 𝑥 ∣ ⊥ } ↔ 𝜓 ) )
10	8 9	bitri	⊢ ( ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝑦 ∈ { 𝑥 ∣ ⊥ } ) ↔ ( 𝑦 ∈ { 𝑥 ∣ ⊥ } ↔ 𝜓 ) )
11	10	albii	⊢ ( ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝑦 ∈ { 𝑥 ∣ ⊥ } ) ↔ ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∣ ⊥ } ↔ 𝜓 ) )
12	4 11	bitri	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ ⊥ } ↔ ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∣ ⊥ } ↔ 𝜓 ) )
13		df-clab	⊢ ( 𝑦 ∈ { 𝑥 ∣ ⊥ } ↔ [ 𝑦 / 𝑥 ] ⊥ )
14		sbv	⊢ ( [ 𝑦 / 𝑥 ] ⊥ ↔ ⊥ )
15	13 14	bitri	⊢ ( 𝑦 ∈ { 𝑥 ∣ ⊥ } ↔ ⊥ )
16	15	bibi1i	⊢ ( ( 𝑦 ∈ { 𝑥 ∣ ⊥ } ↔ 𝜓 ) ↔ ( ⊥ ↔ 𝜓 ) )
17	16	albii	⊢ ( ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∣ ⊥ } ↔ 𝜓 ) ↔ ∀ 𝑦 ( ⊥ ↔ 𝜓 ) )
18		falim	⊢ ( ⊥ → ( 𝜓 → ¬ 𝜓 ) )
19		idd	⊢ ( ¬ ⊥ → ( ¬ 𝜓 → ¬ 𝜓 ) )
20	18 19	bija	⊢ ( ( ⊥ ↔ 𝜓 ) → ¬ 𝜓 )
21		falim	⊢ ( ⊥ → 𝜓 )
22		id	⊢ ( 𝜓 → 𝜓 )
23	21 22	pm5.21ni	⊢ ( ¬ 𝜓 → ( ⊥ ↔ 𝜓 ) )
24	20 23	impbii	⊢ ( ( ⊥ ↔ 𝜓 ) ↔ ¬ 𝜓 )
25	24	albii	⊢ ( ∀ 𝑦 ( ⊥ ↔ 𝜓 ) ↔ ∀ 𝑦 ¬ 𝜓 )
26	17 25	bitri	⊢ ( ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∣ ⊥ } ↔ 𝜓 ) ↔ ∀ 𝑦 ¬ 𝜓 )
27	12 26	bitri	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ ⊥ } ↔ ∀ 𝑦 ¬ 𝜓 )
28	3 27	bitri	⊢ ( { 𝑥 ∣ 𝜑 } = ∅ ↔ ∀ 𝑦 ¬ 𝜓 )