Theorem ralf0

Description: The quantification of a falsehood is vacuous when true. (Contributed by NM, 26-Nov-2005) (Proof shortened by JJ, 14-Jul-2021) Avoid df-clel , ax-8 . (Revised by Gino Giotto, 2-Sep-2024)

	Ref	Expression
Hypothesis	ralf0.1	⊢ ¬ 𝜑
Assertion	ralf0	⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ 𝐴 = ∅ )

Proof

Step	Hyp	Ref	Expression
1		ralf0.1	⊢ ¬ 𝜑
2		r19.26	⊢ ( ∀ 𝑥 ∈ 𝐴 ( ¬ 𝜑 ∧ 𝜑 ) ↔ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝜑 ) )
3		pm2.24	⊢ ( 𝜑 → ( ¬ 𝜑 → ⊥ ) )
4	3	impcom	⊢ ( ( ¬ 𝜑 ∧ 𝜑 ) → ⊥ )
5	4	ralimi	⊢ ( ∀ 𝑥 ∈ 𝐴 ( ¬ 𝜑 ∧ 𝜑 ) → ∀ 𝑥 ∈ 𝐴 ⊥ )
6		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐴 ⊥ ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ⊥ ) )
7		dfnot	⊢ ( ¬ 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ 𝐴 → ⊥ ) )
8	7	bicomi	⊢ ( ( 𝑥 ∈ 𝐴 → ⊥ ) ↔ ¬ 𝑥 ∈ 𝐴 )
9	8	albii	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ⊥ ) ↔ ∀ 𝑥 ¬ 𝑥 ∈ 𝐴 )
10	6 9	sylbb	⊢ ( ∀ 𝑥 ∈ 𝐴 ⊥ → ∀ 𝑥 ¬ 𝑥 ∈ 𝐴 )
11		id	⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐴 )
12		falim	⊢ ( ⊥ → 𝑥 ∈ 𝐴 )
13	11 12	pm5.21ni	⊢ ( ¬ 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐴 ↔ ⊥ ) )
14		df-clab	⊢ ( 𝑥 ∈ { 𝑦 ∣ ⊥ } ↔ [ 𝑥 / 𝑦 ] ⊥ )
15		sbv	⊢ ( [ 𝑥 / 𝑦 ] ⊥ ↔ ⊥ )
16	14 15	bitri	⊢ ( 𝑥 ∈ { 𝑦 ∣ ⊥ } ↔ ⊥ )
17	13 16	bitr4di	⊢ ( ¬ 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ { 𝑦 ∣ ⊥ } ) )
18	17	alimi	⊢ ( ∀ 𝑥 ¬ 𝑥 ∈ 𝐴 → ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ { 𝑦 ∣ ⊥ } ) )
19		dfcleq	⊢ ( 𝐴 = { 𝑦 ∣ ⊥ } ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ { 𝑦 ∣ ⊥ } ) )
20	18 19	sylibr	⊢ ( ∀ 𝑥 ¬ 𝑥 ∈ 𝐴 → 𝐴 = { 𝑦 ∣ ⊥ } )
21		dfnul4	⊢ ∅ = { 𝑦 ∣ ⊥ }
22	20 21	eqtr4di	⊢ ( ∀ 𝑥 ¬ 𝑥 ∈ 𝐴 → 𝐴 = ∅ )
23	5 10 22	3syl	⊢ ( ∀ 𝑥 ∈ 𝐴 ( ¬ 𝜑 ∧ 𝜑 ) → 𝐴 = ∅ )
24	2 23	sylbir	⊢ ( ( ∀ 𝑥 ∈ 𝐴 ¬ 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝜑 ) → 𝐴 = ∅ )
25	24	ex	⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝜑 → ( ∀ 𝑥 ∈ 𝐴 𝜑 → 𝐴 = ∅ ) )
26	1	a1i	⊢ ( 𝑥 ∈ 𝐴 → ¬ 𝜑 )
27	25 26	mprg	⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 → 𝐴 = ∅ )
28		rzal	⊢ ( 𝐴 = ∅ → ∀ 𝑥 ∈ 𝐴 𝜑 )
29	27 28	impbii	⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ 𝐴 = ∅ )