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

Theorem nfex 2262
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 2262, hbex 2263. (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 1743 . 2 (∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑)
2 nfex.1 . . . . 5 𝑥𝜑
32nfn 1819 . . . 4 𝑥 ¬ 𝜑
43nfal 2261 . . 3 𝑥𝑦 ¬ 𝜑
54nfn 1819 . 2 𝑥 ¬ ∀𝑦 ¬ 𝜑
61, 5nfxfr 1815 1 𝑥𝑦𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wal 1505  wex 1742  wnf 1746
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-10 2077  ax-11 2091  ax-12 2104
This theorem depends on definitions:  df-bi 199  df-or 834  df-ex 1743  df-nf 1747
This theorem is referenced by:  hbex  2263  nfnf  2264  19.12  2265  eeor  2272  eean  2280  eeeanv  2282  nfmo1  2566  nfeu1  2602  2moswapv  2657  moexex  2664  r19.12  3259  ceqsex2  3458  nfopab  4991  nfopab2  4993  cbvopab1  4996  cbvopab1s  4998  axrep2  5046  axrep3  5047  axrep4  5048  copsex2t  5232  copsex2g  5233  mosubopt  5249  euotd  5252  nfco  5579  dfdmf  5608  dfrnf  5656  nfdm  5659  fv3  6511  oprabv  7027  nfoprab2  7029  nfoprab3  7030  nfoprab  7031  cbvoprab1  7051  cbvoprab2  7052  cbvoprab3  7055  nfwrecs  7745  ac6sfi  8549  aceq1  9329  zfcndrep  9826  zfcndinf  9830  nfsum1  14897  nfsum  14898  fsum2dlem  14975  nfcprod1  15114  nfcprod  15115  fprod2dlem  15184  brabgaf  30113  cnvoprabOLD  30197  bnj981  31830  bnj1388  31911  bnj1445  31922  bnj1489  31934  nffrecs  32581  bj-axrep2  33559  bj-axrep3  33560  bj-axrep4  33561  pm11.71  40090  upbdrech  40947  stoweidlem57  41719  or2expropbi  42620  ich2exprop  42941  ichnreuop  42942  ichreuopeq  42943  reuopreuprim  42996
  Copyright terms: Public domain W3C validator