![]() |
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 2218 | . . 3 ⊢ (𝜑 → ∀𝑥𝜑) |
3 | 2 | hbal 2191 | . 2 ⊢ (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑) |
4 | 3 | nf5i 2178 | 1 ⊢ Ⅎ𝑥∀𝑦𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ∀wal 1628 Ⅎwnf 1855 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1869 ax-4 1884 ax-5 1990 ax-6 2056 ax-7 2092 ax-10 2173 ax-11 2189 ax-12 2202 |
This theorem depends on definitions: df-bi 197 df-ex 1852 df-nf 1857 |
This theorem is referenced by: nfex 2317 nfnf 2321 nfaldOLD 2327 nfa2OLD 2329 aaan 2330 cbv3v 2332 pm11.53 2340 19.12vv 2341 cbv3 2425 cbval2 2437 nfsb4t 2535 euf 2625 mo2 2626 2eu3 2703 bm1.1 2755 nfnfc1 2915 nfnfc 2922 nfnfcALT 2923 sbcnestgf 4137 nfdisj 4764 nfdisj1 4765 axrep1 4903 axrep2 4904 axrep3 4905 axrep4 4906 nffr 5223 zfcndrep 9637 zfcndinf 9641 mreexexd 16515 mptelee 25995 mo5f 29658 19.12b 32037 bj-cbv2v 33062 bj-cbval2v 33067 bj-axrep1 33118 bj-axrep2 33119 bj-axrep3 33120 bj-axrep4 33121 ax11-pm2 33152 wl-sb8t 33661 wl-mo2tf 33680 wl-eutf 33682 wl-mo2t 33684 wl-mo3t 33685 wl-sb8eut 33686 mpt2bi123f 34296 pm11.57 39108 pm11.59 39110 nfsetrecs 42951 |
Copyright terms: Public domain | W3C validator |