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 𝜑, 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 2065 | . . 3 ⊢ (𝜑 → ∀𝑥𝜑) |
3 | 2 | hbal 2036 | . 2 ⊢ (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑) |
4 | 3 | nf5i 2024 | 1 ⊢ Ⅎ𝑥∀𝑦𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ∀wal 1481 Ⅎwnf 1708 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-10 2019 ax-11 2034 ax-12 2047 |
This theorem depends on definitions: df-bi 197 df-ex 1705 df-nf 1710 |
This theorem is referenced by: nfex 2154 nfnf 2158 nfaldOLD 2166 nfa2OLD 2168 aaan 2170 cbv3v 2172 pm11.53 2179 19.12vv 2180 cbv3 2265 cbval2 2279 nfsb4t 2389 euf 2478 mo2 2479 2eu3 2555 bm1.1 2607 nfnfc1 2767 nfnfc 2774 nfnfcALT 2775 sbcnestgf 3995 dfnfc2OLD 4455 nfdisj 4632 nfdisj1 4633 axrep1 4772 axrep2 4773 axrep3 4774 axrep4 4775 nffr 5088 zfcndrep 9436 zfcndinf 9440 mreexexd 16308 mreexexdOLD 16309 mptelee 25775 mo5f 29324 19.12b 31707 bj-cbv2v 32732 bj-cbval2v 32737 bj-axrep1 32788 bj-axrep2 32789 bj-axrep3 32790 bj-axrep4 32791 ax11-pm2 32823 bj-nfnfc 32853 wl-sb8t 33333 wl-mo2tf 33353 wl-eutf 33355 wl-mo2t 33357 wl-mo3t 33358 wl-sb8eut 33359 mpt2bi123f 33971 pm11.57 38589 pm11.59 38591 nfsetrecs 42433 |
Copyright terms: Public domain | W3C validator |