# Metamath Proof Explorer

## 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{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
Assertion nfnfc ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{A}$

### Proof

Step Hyp Ref Expression
1 nfnfc.1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
2 df-nfc ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{A}↔\forall {z}\phantom{\rule{.4em}{0ex}}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{z}\in {A}$
3 df-nfc ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}↔\forall {z}\phantom{\rule{.4em}{0ex}}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{z}\in {A}$
4 1 3 mpbi ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{z}\in {A}$
5 4 spi ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{z}\in {A}$
6 5 nfnf ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{z}\in {A}$
7 6 nfal ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{z}\in {A}$
8 2 7 nfxfr ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{A}$