This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 GG, 2-Sep-2024)

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

Proof

Step	Hyp	Ref	Expression
1		pm2.21	⊢ ( ¬ 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐴 → 𝜑 ) )
2	1	alimi	⊢ ( ∀ 𝑥 ¬ 𝑥 ∈ 𝐴 → ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) )
3		eq0	⊢ ( 𝐴 = ∅ ↔ ∀ 𝑥 ¬ 𝑥 ∈ 𝐴 )
4		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) )
5	2 3 4	3imtr4i	⊢ ( 𝐴 = ∅ → ∀ 𝑥 ∈ 𝐴 𝜑 )