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

Metamath Proof Explorer

Theorem rzalf

Description: A version of rzal using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017)

		Ref	Expression
	Hypothesis	rzalf.1	⊢ Ⅎ 𝑥 𝐴 = ∅
	Assertion	rzalf	⊢ ( 𝐴 = ∅ → ∀ 𝑥 ∈ 𝐴 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		rzalf.1	⊢ Ⅎ 𝑥 𝐴 = ∅
2		ne0i	⊢ ( 𝑥 ∈ 𝐴 → 𝐴 ≠ ∅ )
3	2	necon2bi	⊢ ( 𝐴 = ∅ → ¬ 𝑥 ∈ 𝐴 )
4	3	pm2.21d	⊢ ( 𝐴 = ∅ → ( 𝑥 ∈ 𝐴 → 𝜑 ) )
5	1 4	ralrimi	⊢ ( 𝐴 = ∅ → ∀ 𝑥 ∈ 𝐴 𝜑 )