Theorem ral0

Description: Vacuous universal quantification is always true. (Contributed by NM, 20-Oct-2005) Avoid df-clel , ax-8 . (Revised by Gino Giotto, 2-Sep-2024)

	Ref	Expression
Assertion	ral0	⊢ ∀ 𝑥 ∈ ∅ 𝜑

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ∅ = ∅
2		rzal	⊢ ( ∅ = ∅ → ∀ 𝑥 ∈ ∅ 𝜑 )
3	1 2	ax-mp	⊢ ∀ 𝑥 ∈ ∅ 𝜑