This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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