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

Theorem nfex 2330
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 2330, hbex 2332. (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 1860 . 2 (∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑)
2 nfex.1 . . . . 5 𝑥𝜑
32nfn 1944 . . . 4 𝑥 ¬ 𝜑
43nfal 2329 . . 3 𝑥𝑦 ¬ 𝜑
54nfn 1944 . 2 𝑥 ¬ ∀𝑦 ¬ 𝜑
61, 5nfxfr 1938 1 𝑥𝑦𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wal 1635  wex 1859  wnf 1863
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-10 2185  ax-11 2201  ax-12 2214
This theorem depends on definitions:  df-bi 198  df-or 866  df-ex 1860  df-nf 1864
This theorem is referenced by:  hbex  2332  nfnf  2334  19.12  2338  eeor  2344  eean  2355  eeeanv  2357  nfeu1  2642  moexex  2705  ceqsex2  3438  nfopab  4912  nfopab2  4914  cbvopab1  4917  cbvopab1s  4919  axrep2  4967  axrep3  4968  axrep4  4969  copsex2t  5146  copsex2g  5147  mosubopt  5165  euotd  5168  nfco  5489  dfdmf  5518  dfrnf  5565  nfdm  5568  fv3  6426  oprabv  6933  nfoprab2  6935  nfoprab3  6936  nfoprab  6937  cbvoprab1  6957  cbvoprab2  6958  cbvoprab3  6961  nfwrecs  7644  ac6sfi  8443  aceq1  9223  zfcndrep  9721  zfcndinf  9725  nfsum1  14643  nfsum  14644  fsum2dlem  14724  nfcprod1  14861  nfcprod  14862  fprod2dlem  14931  brabgaf  29745  cnvoprabOLD  29825  bnj981  31343  bnj1388  31424  bnj1445  31435  bnj1489  31447  nffrecs  32099  bj-axrep2  33103  bj-axrep3  33104  bj-axrep4  33105  pm11.71  39097  upbdrech  40000  stoweidlem57  40753
  Copyright terms: Public domain W3C validator