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		df-nfc	⊢ ( Ⅎ 𝑥 𝐴 ↔ ∀ 𝑧 Ⅎ 𝑥 𝑧 ∈ 𝐴 )
4	1 3	mpbi	⊢ ∀ 𝑧 Ⅎ 𝑥 𝑧 ∈ 𝐴
5	4	spi	⊢ Ⅎ 𝑥 𝑧 ∈ 𝐴
6	5	nfnf	⊢ Ⅎ 𝑥 Ⅎ 𝑦 𝑧 ∈ 𝐴
7	6	nfal	⊢ Ⅎ 𝑥 ∀ 𝑧 Ⅎ 𝑦 𝑧 ∈ 𝐴
8	2 7	nfxfr	⊢ Ⅎ 𝑥 Ⅎ 𝑦 𝐴