| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > nfal | Structured version Visualization version GIF version | ||
| Description: If 𝑥 is not free in 𝜑, then it is not free in ∀𝑦𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) |
| Ref | Expression |
|---|---|
| nfal.1 | ⊢ Ⅎ𝑥𝜑 |
| Ref | Expression |
|---|---|
| nfal | ⊢ Ⅎ𝑥∀𝑦𝜑 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfal.1 | . . . 4 ⊢ Ⅎ𝑥𝜑 | |
| 2 | 1 | nf5ri 2195 | . . 3 ⊢ (𝜑 → ∀𝑥𝜑) |
| 3 | 2 | hbal 2167 | . 2 ⊢ (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑) |
| 4 | 3 | nf5i 2146 | 1 ⊢ Ⅎ𝑥∀𝑦𝜑 |
| Colors of variables: wff setvar class |
| Syntax hints: ∀wal 1538 Ⅎwnf 1783 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-10 2141 ax-11 2157 ax-12 2177 |
| This theorem depends on definitions: df-bi 207 df-ex 1780 df-nf 1784 |
| This theorem is referenced by: nfex 2324 nfnf 2326 nfsbvOLD 2331 aaanOLD 2334 cbval2v 2345 pm11.53 2348 19.12vv 2349 cbval2 2416 nfsb4t 2504 mof 2563 euf 2576 2eu3 2654 axextmo 2712 nfnfc1 2908 nfnfc 2918 sbcnestgfw 4421 sbcnestgf 4426 nfdisjw 5122 nfdisj 5123 nfdisj1 5124 axrep1 5280 axrep2 5282 axrep3 5283 axrep4OLD 5286 nffr 5658 zfcndrep 10654 zfcndinf 10658 mreexexd 17691 mptelee 28910 mo5f 32508 iinabrex 32582 19.12b 35802 bj-cbv2v 36799 ax11-pm2 36837 wl-sb8t 37553 wl-mo2tf 37572 wl-eutf 37574 wl-mo2t 37576 wl-mo3t 37577 wl-sb8eut 37579 wl-sb8eutv 37580 mpobi123f 38169 pm11.57 44408 pm11.59 44410 ichnfimlem 47450 ichnfim 47451 nfsetrecs 49205 pgind 49236 |
| Copyright terms: Public domain | W3C validator |