Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > nfex | Structured version Visualization version GIF version |
Description: If 𝑥 is not free in 𝜑, it is not free in ∃𝑦𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.) Reduce symbol count in nfex 2334, hbex 2335. (Revised by Wolf Lammen, 16-Oct-2021.) |
Ref | Expression |
---|---|
nfex.1 | ⊢ Ⅎ𝑥𝜑 |
Ref | Expression |
---|---|
nfex | ⊢ Ⅎ𝑥∃𝑦𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ex 1772 | . 2 ⊢ (∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑) | |
2 | nfex.1 | . . . . 5 ⊢ Ⅎ𝑥𝜑 | |
3 | 2 | nfn 1848 | . . . 4 ⊢ Ⅎ𝑥 ¬ 𝜑 |
4 | 3 | nfal 2333 | . . 3 ⊢ Ⅎ𝑥∀𝑦 ¬ 𝜑 |
5 | 4 | nfn 1848 | . 2 ⊢ Ⅎ𝑥 ¬ ∀𝑦 ¬ 𝜑 |
6 | 1, 5 | nfxfr 1844 | 1 ⊢ Ⅎ𝑥∃𝑦𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∀wal 1526 ∃wex 1771 Ⅎwnf 1775 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-10 2136 ax-11 2151 ax-12 2167 |
This theorem depends on definitions: df-bi 208 df-or 842 df-ex 1772 df-nf 1776 |
This theorem is referenced by: hbex 2335 nfnf 2336 19.12 2337 eeor 2345 eean 2360 eeeanv 2362 nfmo1 2634 nfeu1 2667 moexexlem 2704 r19.12 3321 ceqsex2 3541 nfopab 5125 nfopab2 5127 cbvopab1 5130 cbvopab1g 5131 cbvopab1s 5133 axrep2 5184 axrep3 5185 axrep4 5186 copsex2t 5374 copsex2g 5375 mosubopt 5391 euotd 5394 nfco 5729 dfdmf 5758 dfrnf 5813 nfdm 5816 fv3 6681 oprabv 7203 nfoprab2 7205 nfoprab3 7206 nfoprab 7207 cbvoprab1 7230 cbvoprab2 7231 cbvoprab3 7234 nfwrecs 7938 ac6sfi 8750 aceq1 9531 zfcndrep 10024 zfcndinf 10028 nfsum1 15034 nfsumw 15035 nfsum 15036 fsum2dlem 15113 nfcprod1 15252 nfcprod 15253 fprod2dlem 15322 brabgaf 30287 cnvoprabOLD 30382 bnj981 32121 bnj1388 32202 bnj1445 32213 bnj1489 32225 nffrecs 33017 pm11.71 40606 upbdrech 41448 stoweidlem57 42219 or2expropbi 43146 ich2exprop 43510 ichnreuop 43511 ichreuopeq 43512 reuopreuprim 43565 |
Copyright terms: Public domain | W3C validator |