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		df-clab	⊢ ( 𝑦 ∈ { 𝑥 ∣ ⊥ } ↔ [ 𝑦 / 𝑥 ] ⊥ )
5		sbv	⊢ ( [ 𝑦 / 𝑥 ] ⊥ ↔ ⊥ )
6	4 5	bitri	⊢ ( 𝑦 ∈ { 𝑥 ∣ ⊥ } ↔ ⊥ )
7	6	bibi2i	⊢ ( ( 𝜓 ↔ 𝑦 ∈ { 𝑥 ∣ ⊥ } ) ↔ ( 𝜓 ↔ ⊥ ) )
8	7	albii	⊢ ( ∀ 𝑦 ( 𝜓 ↔ 𝑦 ∈ { 𝑥 ∣ ⊥ } ) ↔ ∀ 𝑦 ( 𝜓 ↔ ⊥ ) )
9	1	eqabcbw	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ ⊥ } ↔ ∀ 𝑦 ( 𝜓 ↔ 𝑦 ∈ { 𝑥 ∣ ⊥ } ) )
10		nbfal	⊢ ( ¬ 𝜓 ↔ ( 𝜓 ↔ ⊥ ) )
11	10	albii	⊢ ( ∀ 𝑦 ¬ 𝜓 ↔ ∀ 𝑦 ( 𝜓 ↔ ⊥ ) )
12	8 9 11	3bitr4i	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ ⊥ } ↔ ∀ 𝑦 ¬ 𝜓 )
13	3 12	bitri	⊢ ( { 𝑥 ∣ 𝜑 } = ∅ ↔ ∀ 𝑦 ¬ 𝜓 )

Metamath Proof Explorer

Theorem ab0w

Proof