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	$$⊢\underset{\_}{Ⅎ}xA$$
Assertion	nfnfc	$$⊢Ⅎx\underset{\_}{Ⅎ}yA$$

Proof

Step	Hyp	Ref	Expression
1		nfnfc.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		df-nfc	$$⊢\underset{\_}{Ⅎ}yA\leftrightarrow \forall zℲyz\in A$$
3		df-nfc	$$⊢\underset{\_}{Ⅎ}xA\leftrightarrow \forall zℲxz\in A$$
4	1 3	mpbi	$$⊢\forall zℲxz\in A$$
5	4	spi	$$⊢Ⅎxz\in A$$
6	5	nfnf	$$⊢ℲxℲyz\in A$$
7	6	nfal	$$⊢Ⅎx\forall zℲyz\in A$$
8	2 7	nfxfr	$$⊢Ⅎx\underset{\_}{Ⅎ}yA$$