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

Theorem nfex 2322
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 2322, hbex 2323. (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 1787 . 2 (∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑)
2 nfex.1 . . . . 5 𝑥𝜑
32nfn 1864 . . . 4 𝑥 ¬ 𝜑
43nfal 2321 . . 3 𝑥𝑦 ¬ 𝜑
54nfn 1864 . 2 𝑥 ¬ ∀𝑦 ¬ 𝜑
61, 5nfxfr 1859 1 𝑥𝑦𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wal 1540  wex 1786  wnf 1790
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-10 2141  ax-11 2158  ax-12 2175
This theorem depends on definitions:  df-bi 206  df-or 845  df-ex 1787  df-nf 1791
This theorem is referenced by:  hbex  2323  nfnf  2324  19.12  2325  eeorOLD  2335  eean  2350  eeeanv  2352  nfmo1  2559  nfeu1  2590  moexexlem  2630  r19.12  3255  r19.12OLD  3256  ceqsex2  3481  nfopab2  5150  cbvopab1  5154  cbvopab1g  5155  cbvopab1s  5157  axrep2  5217  axrep3  5218  axrep4  5219  copsex2t  5410  copsex2gOLD  5412  mosubopt  5428  euotd  5431  nfco  5773  dfdmf  5804  dfrnf  5858  nfdm  5859  fv3  6789  oprabv  7330  nfoprab2  7332  nfoprab3  7333  nfoprab  7334  cbvoprab1  7357  cbvoprab2  7358  cbvoprab3  7361  nffrecs  8091  nfwrecsOLD  8125  ac6sfi  9046  aceq1  9884  zfcndrep  10381  zfcndinf  10385  nfsum1  15412  nfsum  15413  nfsumOLD  15414  fsum2dlem  15493  nfcprod1  15631  nfcprod  15632  fprod2dlem  15701  brabgaf  30957  2ndresdju  30995  cnvoprabOLD  31064  bnj981  32939  bnj1388  33022  bnj1445  33033  bnj1489  33045  fineqvrep  33073  bj-opabco  35368  pm11.71  41997  upbdrech  42826  stoweidlem57  43580  or2expropbi  44507  ich2exprop  44902  ichnreuop  44903  ichreuopeq  44904  reuopreuprim  44957
  Copyright terms: Public domain W3C validator