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	⊢ ( Ⅎ 𝑥 𝐴 → Ⅎ 𝑥 𝑦 ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		df-nfc	⊢ ( Ⅎ 𝑥 𝐴 ↔ ∀ 𝑦 Ⅎ 𝑥 𝑦 ∈ 𝐴 )
2		sp	⊢ ( ∀ 𝑦 Ⅎ 𝑥 𝑦 ∈ 𝐴 → Ⅎ 𝑥 𝑦 ∈ 𝐴 )
3	1 2	sylbi	⊢ ( Ⅎ 𝑥 𝐴 → Ⅎ 𝑥 𝑦 ∈ 𝐴 )