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

Theorem nfex 2312
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.)
Hypothesis
Ref Expression
nfex.1 𝑥𝜑
Assertion
Ref Expression
nfex 𝑥𝑦𝜑

Proof of Theorem nfex
StepHypRef Expression
1 df-ex 1774 . 2 (∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑)
2 nfex.1 . . . . 5 𝑥𝜑
32nfn 1852 . . . 4 𝑥 ¬ 𝜑
43nfal 2311 . . 3 𝑥𝑦 ¬ 𝜑
54nfn 1852 . 2 𝑥 ¬ ∀𝑦 ¬ 𝜑
61, 5nfxfr 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