![]() |
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 2262, hbex 2263. (Revised by Wolf Lammen, 16-Oct-2021.) |
Ref | Expression |
---|---|
nfex.1 | ⊢ Ⅎ𝑥𝜑 |
Ref | Expression |
---|---|
nfex | ⊢ Ⅎ𝑥∃𝑦𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ex 1743 | . 2 ⊢ (∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑) | |
2 | nfex.1 | . . . . 5 ⊢ Ⅎ𝑥𝜑 | |
3 | 2 | nfn 1819 | . . . 4 ⊢ Ⅎ𝑥 ¬ 𝜑 |
4 | 3 | nfal 2261 | . . 3 ⊢ Ⅎ𝑥∀𝑦 ¬ 𝜑 |
5 | 4 | nfn 1819 | . 2 ⊢ Ⅎ𝑥 ¬ ∀𝑦 ¬ 𝜑 |
6 | 1, 5 | nfxfr 1815 | 1 ⊢ Ⅎ𝑥∃𝑦𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∀wal 1505 ∃wex 1742 Ⅎwnf 1746 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1964 ax-10 2077 ax-11 2091 ax-12 2104 |
This theorem depends on definitions: df-bi 199 df-or 834 df-ex 1743 df-nf 1747 |
This theorem is referenced by: hbex 2263 nfnf 2264 19.12 2265 eeor 2272 eean 2280 eeeanv 2282 nfmo1 2566 nfeu1 2602 2moswapv 2657 moexex 2664 r19.12 3259 ceqsex2 3458 nfopab 4991 nfopab2 4993 cbvopab1 4996 cbvopab1s 4998 axrep2 5046 axrep3 5047 axrep4 5048 copsex2t 5232 copsex2g 5233 mosubopt 5249 euotd 5252 nfco 5579 dfdmf 5608 dfrnf 5656 nfdm 5659 fv3 6511 oprabv 7027 nfoprab2 7029 nfoprab3 7030 nfoprab 7031 cbvoprab1 7051 cbvoprab2 7052 cbvoprab3 7055 nfwrecs 7745 ac6sfi 8549 aceq1 9329 zfcndrep 9826 zfcndinf 9830 nfsum1 14897 nfsum 14898 fsum2dlem 14975 nfcprod1 15114 nfcprod 15115 fprod2dlem 15184 brabgaf 30113 cnvoprabOLD 30197 bnj981 31830 bnj1388 31911 bnj1445 31922 bnj1489 31934 nffrecs 32581 bj-axrep2 33559 bj-axrep3 33560 bj-axrep4 33561 pm11.71 40090 upbdrech 40947 stoweidlem57 41719 or2expropbi 42620 ich2exprop 42941 ichnreuop 42942 ichreuopeq 42943 reuopreuprim 42996 |
Copyright terms: Public domain | W3C validator |