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 | |- F/_ x A |
|
| Assertion | nfnfc | |- F/ x F/_ y A |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfnfc.1 | |- F/_ x A |
|
| 2 | df-nfc | |- ( F/_ y A <-> A. z F/ y z e. A ) |
|
| 3 | df-nfc | |- ( F/_ x A <-> A. z F/ x z e. A ) |
|
| 4 | 1 3 | mpbi | |- A. z F/ x z e. A |
| 5 | 4 | spi | |- F/ x z e. A |
| 6 | 5 | nfnf | |- F/ x F/ y z e. A |
| 7 | 6 | nfal | |- F/ x A. z F/ y z e. A |
| 8 | 2 7 | nfxfr | |- F/ x F/_ y A |