![]() |
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 2318, hbex 2319. (Revised by Wolf Lammen, 16-Oct-2021.) |
Ref | Expression |
---|---|
nfex.1 | ⊢ Ⅎ𝑥𝜑 |
Ref | Expression |
---|---|
nfex | ⊢ Ⅎ𝑥∃𝑦𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ex 1783 | . 2 ⊢ (∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑) | |
2 | nfex.1 | . . . . 5 ⊢ Ⅎ𝑥𝜑 | |
3 | 2 | nfn 1861 | . . . 4 ⊢ Ⅎ𝑥 ¬ 𝜑 |
4 | 3 | nfal 2317 | . . 3 ⊢ Ⅎ𝑥∀𝑦 ¬ 𝜑 |
5 | 4 | nfn 1861 | . 2 ⊢ Ⅎ𝑥 ¬ ∀𝑦 ¬ 𝜑 |
6 | 1, 5 | nfxfr 1856 | 1 ⊢ Ⅎ𝑥∃𝑦𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∀wal 1540 ∃wex 1782 Ⅎwnf 1786 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-10 2138 ax-11 2155 ax-12 2172 |
This theorem depends on definitions: df-bi 206 df-or 847 df-ex 1783 df-nf 1787 |
This theorem is referenced by: hbex 2319 nfnf 2320 19.12 2321 eeorOLD 2331 eean 2345 eeeanv 2347 nfmo1 2556 nfeu1 2587 moexexlem 2627 r19.12 3300 r19.12OLD 3301 ceqsex2 3501 nfopab2 5181 cbvopab1 5185 cbvopab1g 5186 cbvopab1s 5188 axrep2 5250 axrep3 5251 axrep4 5252 copsex2t 5454 copsex2gOLD 5456 mosubopt 5472 euotd 5475 nfco 5826 dfdmf 5857 dfrnf 5910 nfdm 5911 fv3 6865 oprabv 7422 nfoprab2 7424 nfoprab3 7425 nfoprab 7426 cbvoprab1 7449 cbvoprab2 7450 cbvoprab3 7453 nffrecs 8219 nfwrecsOLD 8253 ac6sfi 9238 aceq1 10060 zfcndrep 10557 zfcndinf 10561 nfsum1 15581 nfsum 15582 nfsumOLD 15583 fsum2dlem 15662 nfcprod1 15800 nfcprod 15801 fprod2dlem 15870 brabgaf 31569 2ndresdju 31607 cnvoprabOLD 31679 bnj981 33602 bnj1388 33685 bnj1445 33696 bnj1489 33708 fineqvrep 33736 bj-opabco 35688 pm11.71 42751 upbdrech 43613 stoweidlem57 44372 or2expropbi 45342 ich2exprop 45737 ichnreuop 45738 ichreuopeq 45739 reuopreuprim 45792 pgind 47236 |
Copyright terms: Public domain | W3C validator |