Theorem rzal

Description: Vacuous quantification is always true. (Contributed by NM, 11-Mar-1997) (Proof shortened by Andrew Salmon, 26-Jun-2011) Avoid df-clel , ax-8 . (Revised by Gino Giotto, 2-Sep-2024)

	Ref	Expression
Assertion	rzal	⊢ ( 𝐴 = ∅ → ∀ 𝑥 ∈ 𝐴 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		dfcleq	⊢ ( 𝐴 = { 𝑦 ∣ ⊥ } ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ { 𝑦 ∣ ⊥ } ) )
2	1	biimpi	⊢ ( 𝐴 = { 𝑦 ∣ ⊥ } → ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ { 𝑦 ∣ ⊥ } ) )
3		df-clab	⊢ ( 𝑥 ∈ { 𝑦 ∣ ⊥ } ↔ [ 𝑥 / 𝑦 ] ⊥ )
4		sbv	⊢ ( [ 𝑥 / 𝑦 ] ⊥ ↔ ⊥ )
5	3 4	bitri	⊢ ( 𝑥 ∈ { 𝑦 ∣ ⊥ } ↔ ⊥ )
6	5	bibi2i	⊢ ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ { 𝑦 ∣ ⊥ } ) ↔ ( 𝑥 ∈ 𝐴 ↔ ⊥ ) )
7		nbfal	⊢ ( ¬ 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ 𝐴 ↔ ⊥ ) )
8		pm2.21	⊢ ( ¬ 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐴 → 𝜑 ) )
9	7 8	sylbir	⊢ ( ( 𝑥 ∈ 𝐴 ↔ ⊥ ) → ( 𝑥 ∈ 𝐴 → 𝜑 ) )
10	6 9	sylbi	⊢ ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ { 𝑦 ∣ ⊥ } ) → ( 𝑥 ∈ 𝐴 → 𝜑 ) )
11	2 10	sylg	⊢ ( 𝐴 = { 𝑦 ∣ ⊥ } → ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) )
12		dfnul4	⊢ ∅ = { 𝑦 ∣ ⊥ }
13	12	eqeq2i	⊢ ( 𝐴 = ∅ ↔ 𝐴 = { 𝑦 ∣ ⊥ } )
14		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) )
15	11 13 14	3imtr4i	⊢ ( 𝐴 = ∅ → ∀ 𝑥 ∈ 𝐴 𝜑 )