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

Theorem nfex 2334
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 2334, hbex 2335. (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 1772 . 2 (∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑)
2 nfex.1 . . . . 5 𝑥𝜑
32nfn 1848 . . . 4 𝑥 ¬ 𝜑
43nfal 2333 . . 3 𝑥𝑦 ¬ 𝜑
54nfn 1848 . 2 𝑥 ¬ ∀𝑦 ¬ 𝜑
61, 5nfxfr 1844 1 𝑥𝑦𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wal 1526  wex 1771  wnf 1775
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-10 2136  ax-11 2151  ax-12 2167
This theorem depends on definitions:  df-bi 208  df-or 842  df-ex 1772  df-nf 1776
This theorem is referenced by:  hbex  2335  nfnf  2336  19.12  2337  eeor  2345  eean  2360  eeeanv  2362  nfmo1  2634  nfeu1  2667  moexexlem  2704  r19.12  3321  ceqsex2  3541  nfopab  5125  nfopab2  5127  cbvopab1  5130  cbvopab1g  5131  cbvopab1s  5133  axrep2  5184  axrep3  5185  axrep4  5186  copsex2t  5374  copsex2g  5375  mosubopt  5391  euotd  5394  nfco  5729  dfdmf  5758  dfrnf  5813  nfdm  5816  fv3  6681  oprabv  7203  nfoprab2  7205  nfoprab3  7206  nfoprab  7207  cbvoprab1  7230  cbvoprab2  7231  cbvoprab3  7234  nfwrecs  7938  ac6sfi  8750  aceq1  9531  zfcndrep  10024  zfcndinf  10028  nfsum1  15034  nfsumw  15035  nfsum  15036  fsum2dlem  15113  nfcprod1  15252  nfcprod  15253  fprod2dlem  15322  brabgaf  30287  cnvoprabOLD  30382  bnj981  32121  bnj1388  32202  bnj1445  32213  bnj1489  32225  nffrecs  33017  pm11.71  40606  upbdrech  41448  stoweidlem57  42219  or2expropbi  43146  ich2exprop  43510  ichnreuop  43511  ichreuopeq  43512  reuopreuprim  43565
  Copyright terms: Public domain W3C validator