| 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 2324, hbex 2325. (Revised by Wolf Lammen, 16-Oct-2021.) |
| Ref | Expression |
|---|---|
| nfex.1 | ⊢ Ⅎ𝑥𝜑 |
| Ref | Expression |
|---|---|
| nfex | ⊢ Ⅎ𝑥∃𝑦𝜑 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-ex 1780 | . 2 ⊢ (∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑) | |
| 2 | nfex.1 | . . . . 5 ⊢ Ⅎ𝑥𝜑 | |
| 3 | 2 | nfn 1857 | . . . 4 ⊢ Ⅎ𝑥 ¬ 𝜑 |
| 4 | 3 | nfal 2323 | . . 3 ⊢ Ⅎ𝑥∀𝑦 ¬ 𝜑 |
| 5 | 4 | nfn 1857 | . 2 ⊢ Ⅎ𝑥 ¬ ∀𝑦 ¬ 𝜑 |
| 6 | 1, 5 | nfxfr 1853 | 1 ⊢ Ⅎ𝑥∃𝑦𝜑 |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 ∀wal 1538 ∃wex 1779 Ⅎwnf 1783 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-10 2141 ax-11 2157 ax-12 2177 |
| This theorem depends on definitions: df-bi 207 df-or 849 df-ex 1780 df-nf 1784 |
| This theorem is referenced by: hbex 2325 nfnf 2326 19.12 2327 eeorOLD 2336 eean 2350 eeeanv 2352 ee4anv 2353 nfmo1 2557 nfeu1 2588 moexexlem 2626 r19.12 3314 r19.12OLD 3315 ceqsex2 3535 nfopab2 5214 cbvopab1 5217 cbvopab1g 5218 cbvopab1s 5220 axrep2 5282 axrep3 5283 axrep4OLD 5286 copsex2t 5497 mosubopt 5515 euotd 5518 nfco 5876 dfdmf 5907 dfrnf 5961 nfdm 5962 fv3 6924 oprabv 7493 nfoprab2 7495 nfoprab3 7496 nfoprab 7497 cbvoprab1 7520 cbvoprab2 7521 cbvoprab3 7524 nffrecs 8308 nfwrecsOLD 8342 ac6sfi 9320 aceq1 10157 zfcndrep 10654 zfcndinf 10658 nfsum1 15726 nfsum 15727 fsum2dlem 15806 nfcprod1 15944 nfcprod 15945 fprod2dlem 16016 brabgaf 32620 2ndresdju 32659 bnj981 34964 bnj1388 35047 bnj1445 35058 bnj1489 35070 fineqvrep 35109 bj-opabco 37189 pm11.71 44416 upbdrech 45317 stoweidlem57 46072 or2expropbi 47046 ich2exprop 47458 ichnreuop 47459 ichreuopeq 47460 reuopreuprim 47513 pgind 49236 |
| Copyright terms: Public domain | W3C validator |