MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfex Structured version   Visualization version   GIF version

Theorem nfex 2345
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 2345, hbex 2346. (Revised by Wolf Lammen, 16-Oct-2021.)
Hypothesis
Ref Expression
nfex.1 𝑥𝜑
Assertion
Ref Expression
nfex 𝑥𝑦𝜑

Proof of Theorem nfex
StepHypRef Expression
1 df-ex 1782 . 2 (∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑)
2 nfex.1 . . . . 5 𝑥𝜑
32nfn 1858 . . . 4 𝑥 ¬ 𝜑
43nfal 2344 . . 3 𝑥𝑦 ¬ 𝜑
54nfn 1858 . 2 𝑥 ¬ ∀𝑦 ¬ 𝜑
61, 5nfxfr 1854 1 𝑥𝑦𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wal 1536  wex 1781  wnf 1785
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-10 2146  ax-11 2162  ax-12 2179
This theorem depends on definitions:  df-bi 210  df-or 845  df-ex 1782  df-nf 1786
This theorem is referenced by:  hbex  2346  nfnf  2347  19.12  2348  eeor  2356  eean  2371  eeeanv  2373  nfmo1  2642  nfeu1  2675  moexexlem  2714  r19.12  3316  ceqsex2  3529  nfopab  5120  nfopab2  5122  cbvopab1  5125  cbvopab1g  5126  cbvopab1s  5128  axrep2  5179  axrep3  5180  axrep4  5181  copsex2t  5370  copsex2g  5371  mosubopt  5387  euotd  5390  nfco  5723  dfdmf  5752  dfrnf  5807  nfdm  5810  fv3  6679  oprabv  7207  nfoprab2  7209  nfoprab3  7210  nfoprab  7211  cbvoprab1  7234  cbvoprab2  7235  cbvoprab3  7238  nfwrecs  7945  ac6sfi  8759  aceq1  9541  zfcndrep  10034  zfcndinf  10038  nfsum1  15046  nfsum  15047  nfsumOLD  15048  fsum2dlem  15125  nfcprod1  15264  nfcprod  15265  fprod2dlem  15334  brabgaf  30370  cnvoprabOLD  30467  bnj981  32279  bnj1388  32362  bnj1445  32373  bnj1489  32385  nffrecs  33177  bj-opabco  34548  pm11.71  41021  upbdrech  41863  stoweidlem57  42625  or2expropbi  43552  ich2exprop  43914  ichnreuop  43915  ichreuopeq  43916  reuopreuprim  43969
  Copyright terms: Public domain W3C validator