Theorem ralf0OLD

Description: Obsolete version of ralf0 as of 2-Sep-2024. (Contributed by NM, 26-Nov-2005) (Proof shortened by JJ, 14-Jul-2021) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	ralf0OLD.1	$$⊢\neg \phi$$
Assertion	ralf0OLD	$$⊢\forall x\in A\phi \leftrightarrow A=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		ralf0OLD.1	$$⊢\neg \phi$$
2		mtt	$$⊢\neg \phi \to \left(\neg x\in A\leftrightarrow \left(x\in A\to \phi \right)\right)$$
3	1 2	ax-mp	$$⊢\neg x\in A\leftrightarrow \left(x\in A\to \phi \right)$$
4	3	albii	$$⊢\forall x\neg x\in A\leftrightarrow \forall x\left(x\in A\to \phi \right)$$
5		eq0	$$⊢A=\varnothing \leftrightarrow \forall x\neg x\in A$$
6		df-ral	$$⊢\forall x\in A\phi \leftrightarrow \forall x\left(x\in A\to \phi \right)$$
7	4 5 6	3bitr4ri	$$⊢\forall x\in A\phi \leftrightarrow A=\varnothing$$