Theorem ab0OLD

Description: Obsolete version of ab0 as of 8-Sep-2024. (Contributed by BJ, 19-Mar-2021) Avoid df-clel , ax-8 . (Revised by Gino Giotto, 30-Aug-2024) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Assertion	ab0OLD	⊢ ( { 𝑥 ∣ 𝜑 } = ∅ ↔ ∀ 𝑥 ¬ 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		dfnul4	⊢ ∅ = { 𝑥 ∣ ⊥ }
2	1	eqeq2i	⊢ ( { 𝑥 ∣ 𝜑 } = ∅ ↔ { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ ⊥ } )
3		dfcleq	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ ⊥ } ↔ ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝑦 ∈ { 𝑥 ∣ ⊥ } ) )
4		df-clab	⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ [ 𝑦 / 𝑥 ] 𝜑 )
5		sb6	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) )
6	4 5	bitri	⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) )
7		df-clab	⊢ ( 𝑦 ∈ { 𝑥 ∣ ⊥ } ↔ [ 𝑦 / 𝑥 ] ⊥ )
8		sbv	⊢ ( [ 𝑦 / 𝑥 ] ⊥ ↔ ⊥ )
9	7 8	bitri	⊢ ( 𝑦 ∈ { 𝑥 ∣ ⊥ } ↔ ⊥ )
10	6 9	bibi12i	⊢ ( ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝑦 ∈ { 𝑥 ∣ ⊥ } ) ↔ ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ↔ ⊥ ) )
11	10	albii	⊢ ( ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝑦 ∈ { 𝑥 ∣ ⊥ } ) ↔ ∀ 𝑦 ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ↔ ⊥ ) )
12		nbfal	⊢ ( ¬ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ↔ ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ↔ ⊥ ) )
13	12	bicomi	⊢ ( ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ↔ ⊥ ) ↔ ¬ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) )
14	13	albii	⊢ ( ∀ 𝑦 ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ↔ ⊥ ) ↔ ∀ 𝑦 ¬ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) )
15		nfna1	⊢ Ⅎ 𝑥 ¬ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 )
16		nfv	⊢ Ⅎ 𝑦 ¬ 𝜑
17		pm2.27	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 = 𝑦 → 𝜑 ) → 𝜑 ) )
18	17	spsd	⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) → 𝜑 ) )
19	18	equcoms	⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) → 𝜑 ) )
20		ax12v	⊢ ( 𝑥 = 𝑦 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )
21	20	equcoms	⊢ ( 𝑦 = 𝑥 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )
22	19 21	impbid	⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ↔ 𝜑 ) )
23	22	notbid	⊢ ( 𝑦 = 𝑥 → ( ¬ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ↔ ¬ 𝜑 ) )
24	15 16 23	cbvalv1	⊢ ( ∀ 𝑦 ¬ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ↔ ∀ 𝑥 ¬ 𝜑 )
25	11 14 24	3bitri	⊢ ( ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝑦 ∈ { 𝑥 ∣ ⊥ } ) ↔ ∀ 𝑥 ¬ 𝜑 )
26	2 3 25	3bitri	⊢ ( { 𝑥 ∣ 𝜑 } = ∅ ↔ ∀ 𝑥 ¬ 𝜑 )