Theorem nfcrALT

Description: Alternate version of nfcr . Avoids ax-8 but uses ax-12 . (Contributed by Mario Carneiro, 11-Aug-2016) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Assertion	nfcrALT	$$⊢\underset{\_}{Ⅎ}xA\to Ⅎxy\in A$$

Proof

Step	Hyp	Ref	Expression
1		df-nfc	$$⊢\underset{\_}{Ⅎ}xA\leftrightarrow \forall yℲxy\in A$$
2		sp	$$⊢\forall yℲxy\in A\to Ⅎxy\in A$$
3	1 2	sylbi	$$⊢\underset{\_}{Ⅎ}xA\to Ⅎxy\in A$$