Theorem rspn0OLD

Description: Obsolete version of rspn0 as of 28-Jun-2024. (Contributed by Alexander van der Vekens, 6-Sep-2018) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	rspn0OLD	$$⊢A\ne \varnothing \to \left(\forall x\in A\phi \to \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		n0	$$⊢A\ne \varnothing \leftrightarrow \exists xx\in A$$
2		nfra1	$$⊢Ⅎx\forall x\in A\phi$$
3		nfv	$$⊢Ⅎx\phi$$
4	2 3	nfim	$$⊢Ⅎx\left(\forall x\in A\phi \to \phi \right)$$
5		rsp	$$⊢\forall x\in A\phi \to \left(x\in A\to \phi \right)$$
6	5	com12	$$⊢x\in A\to \left(\forall x\in A\phi \to \phi \right)$$
7	4 6	exlimi	$$⊢\exists xx\in A\to \left(\forall x\in A\phi \to \phi \right)$$
8	1 7	sylbi	$$⊢A\ne \varnothing \to \left(\forall x\in A\phi \to \phi \right)$$