Theorem nfnfc

Description: Hypothesis builder for F/_ y A . (Contributed by Mario Carneiro, 11-Aug-2016) Remove dependency on ax-13 . (Revised by Wolf Lammen, 10-Dec-2019)

	Ref	Expression
Hypothesis	nfnfc.1	⊢ Ⅎ 𝑥 𝐴
Assertion	nfnfc	⊢ Ⅎ 𝑥 Ⅎ 𝑦 𝐴

Proof

Step	Hyp	Ref	Expression
1		nfnfc.1	⊢ Ⅎ 𝑥 𝐴
2		df-nfc	⊢ ( Ⅎ 𝑦 𝐴 ↔ ∀ 𝑧 Ⅎ 𝑦 𝑧 ∈ 𝐴 )
3	1	nfcriv	⊢ Ⅎ 𝑥 𝑧 ∈ 𝐴
4	3	nfnf	⊢ Ⅎ 𝑥 Ⅎ 𝑦 𝑧 ∈ 𝐴
5	4	nfal	⊢ Ⅎ 𝑥 ∀ 𝑧 Ⅎ 𝑦 𝑧 ∈ 𝐴
6	2 5	nfxfr	⊢ Ⅎ 𝑥 Ⅎ 𝑦 𝐴