![]() |
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 𝜑, then 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 2312, hbex 2313. (Revised by Wolf Lammen, 16-Oct-2021.) |
Ref | Expression |
---|---|
nfex.1 | ⊢ Ⅎ𝑥𝜑 |
Ref | Expression |
---|---|
nfex | ⊢ Ⅎ𝑥∃𝑦𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ex 1774 | . 2 ⊢ (∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑) | |
2 | nfex.1 | . . . . 5 ⊢ Ⅎ𝑥𝜑 | |
3 | 2 | nfn 1852 | . . . 4 ⊢ Ⅎ𝑥 ¬ 𝜑 |
4 | 3 | nfal 2311 | . . 3 ⊢ Ⅎ𝑥∀𝑦 ¬ 𝜑 |
5 | 4 | nfn 1852 | . 2 ⊢ Ⅎ𝑥 ¬ ∀𝑦 ¬ 𝜑 |
6 | 1, 5 | nfxfr 1847 | 1 ⊢ Ⅎ𝑥∃𝑦𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∀wal 1531 ∃wex 1773 Ⅎwnf 1777 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-10 2129 ax-11 2146 ax-12 2166 |
This theorem depends on definitions: df-bi 206 df-or 846 df-ex 1774 df-nf 1778 |
This theorem is referenced by: hbex 2313 nfnf 2314 19.12 2315 eeorOLD 2324 eean 2338 eeeanv 2340 nfmo1 2545 nfeu1 2576 moexexlem 2614 r19.12 3301 r19.12OLD 3302 ceqsex2 3519 nfopab2 5220 cbvopab1 5224 cbvopab1g 5225 cbvopab1s 5227 axrep2 5289 axrep3 5290 axrep4 5291 copsex2t 5494 copsex2gOLD 5496 mosubopt 5512 euotd 5515 nfco 5868 dfdmf 5899 dfrnf 5952 nfdm 5953 fv3 6914 oprabv 7480 nfoprab2 7482 nfoprab3 7483 nfoprab 7484 cbvoprab1 7507 cbvoprab2 7508 cbvoprab3 7511 nffrecs 8289 nfwrecsOLD 8323 ac6sfi 9315 aceq1 10147 zfcndrep 10644 zfcndinf 10648 nfsum1 15677 nfsum 15678 fsum2dlem 15757 nfcprod1 15895 nfcprod 15896 fprod2dlem 15965 brabgaf 32482 2ndresdju 32521 cnvoprabOLD 32589 bnj981 34714 bnj1388 34797 bnj1445 34808 bnj1489 34820 fineqvrep 34848 bj-opabco 36800 pm11.71 43978 upbdrech 44827 stoweidlem57 45585 or2expropbi 46556 ich2exprop 46950 ichnreuop 46951 ichreuopeq 46952 reuopreuprim 47005 pgind 48336 |
Copyright terms: Public domain | W3C validator |