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	$⊢ Ⅎ x A = \emptyset$
	Assertion	rzalf	$⊢ A = \emptyset \to \forall x \in A φ$

Proof

Step	Hyp	Ref	Expression
1		rzalf.1	$⊢ Ⅎ x A = \emptyset$
2		ne0i	$⊢ x \in A \to A \neq \emptyset$
3	2	necon2bi	$⊢ A = \emptyset \to \neg x \in A$
4	3	pm2.21d	$⊢ A = \emptyset \to (x \in A \to φ)$
5	1 4	ralrimi	$⊢ A = \emptyset \to \forall x \in A φ$