![]() |
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 2189 | . . 3 ⊢ (𝜑 → ∀𝑥𝜑) |
3 | 2 | hbal 2168 | . 2 ⊢ (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑) |
4 | 3 | nf5i 2143 | 1 ⊢ Ⅎ𝑥∀𝑦𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ∀wal 1540 Ⅎwnf 1786 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-10 2138 ax-11 2155 ax-12 2172 |
This theorem depends on definitions: df-bi 206 df-ex 1783 df-nf 1787 |
This theorem is referenced by: nfex 2318 nfnf 2320 nfsbvOLD 2325 aaanOLD 2329 cbval2v 2340 pm11.53 2343 19.12vv 2344 cbval2 2411 nfsb4t 2499 mof 2558 euf 2571 2eu3 2650 axextmo 2708 nfnfc1 2907 nfnfc 2916 nfabdwOLD 2928 sbcnestgfw 4417 sbcnestgf 4422 nfdisjw 5124 nfdisj 5125 nfdisj1 5126 axrep1 5285 axrep2 5287 axrep3 5288 axrep4 5289 nffr 5649 zfcndrep 10605 zfcndinf 10609 mreexexd 17588 mptelee 28133 mo5f 31707 iinabrex 31778 19.12b 34711 bj-cbv2v 35614 ax11-pm2 35652 wl-sb8t 36355 wl-mo2tf 36374 wl-eutf 36376 wl-mo2t 36378 wl-mo3t 36379 wl-sb8eut 36380 mpobi123f 36968 pm11.57 43081 pm11.59 43083 ichnfimlem 46066 ichnfim 46067 nfsetrecs 47633 pgind 47664 |
Copyright terms: Public domain | W3C validator |