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

Theorem nfex 2324
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 2324, hbex 2325. (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 1780 . 2 (∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑)
2 nfex.1 . . . . 5 𝑥𝜑
32nfn 1857 . . . 4 𝑥 ¬ 𝜑
43nfal 2323 . . 3 𝑥𝑦 ¬ 𝜑
54nfn 1857 . 2 𝑥 ¬ ∀𝑦 ¬ 𝜑
61, 5nfxfr 1853 1 𝑥𝑦𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wal 1538  wex 1779  wnf 1783
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-10 2141  ax-11 2157  ax-12 2177
This theorem depends on definitions:  df-bi 207  df-or 849  df-ex 1780  df-nf 1784
This theorem is referenced by:  hbex  2325  nfnf  2326  19.12  2327  eeorOLD  2336  eean  2350  eeeanv  2352  ee4anv  2353  nfmo1  2557  nfeu1  2588  moexexlem  2626  r19.12  3314  r19.12OLD  3315  ceqsex2  3535  nfopab2  5214  cbvopab1  5217  cbvopab1g  5218  cbvopab1s  5220  axrep2  5282  axrep3  5283  axrep4OLD  5286  copsex2t  5497  mosubopt  5515  euotd  5518  nfco  5876  dfdmf  5907  dfrnf  5961  nfdm  5962  fv3  6924  oprabv  7493  nfoprab2  7495  nfoprab3  7496  nfoprab  7497  cbvoprab1  7520  cbvoprab2  7521  cbvoprab3  7524  nffrecs  8308  nfwrecsOLD  8342  ac6sfi  9320  aceq1  10157  zfcndrep  10654  zfcndinf  10658  nfsum1  15726  nfsum  15727  fsum2dlem  15806  nfcprod1  15944  nfcprod  15945  fprod2dlem  16016  brabgaf  32620  2ndresdju  32659  bnj981  34964  bnj1388  35047  bnj1445  35058  bnj1489  35070  fineqvrep  35109  bj-opabco  37189  pm11.71  44416  upbdrech  45317  stoweidlem57  46072  or2expropbi  47046  ich2exprop  47458  ichnreuop  47459  ichreuopeq  47460  reuopreuprim  47513  pgind  49236
  Copyright terms: Public domain W3C validator