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

Theorem nfex 2140
 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 2140, hbex 2142. (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 1696 . 2 (∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑)
2 nfex.1 . . . . 5 𝑥𝜑
32nfn 1768 . . . 4 𝑥 ¬ 𝜑
43nfal 2139 . . 3 𝑥𝑦 ¬ 𝜑
54nfn 1768 . 2 𝑥 ¬ ∀𝑦 ¬ 𝜑
61, 5nfxfr 1771 1 𝑥𝑦𝜑
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3  ∀wal 1473  ∃wex 1695  Ⅎwnf 1699 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034 This theorem depends on definitions:  df-bi 196  df-or 384  df-ex 1696  df-nf 1701 This theorem is referenced by:  hbex  2142  nfnf  2144  19.12  2150  eeor  2157  eean  2169  eeeanv  2171  nfeu1  2468  moexex  2529  ceqsex2  3217  nfopab  4650  nfopab2  4652  cbvopab1  4655  cbvopab1s  4657  axrep2  4701  axrep3  4702  axrep4  4703  copsex2t  4883  copsex2g  4884  mosubopt  4897  euotd  4900  nfco  5209  dfdmf  5239  dfrnf  5285  nfdm  5288  fv3  6116  oprabv  6601  nfoprab2  6603  nfoprab3  6604  nfoprab  6605  cbvoprab1  6625  cbvoprab2  6626  cbvoprab3  6629  nfwrecs  7296  ac6sfi  8089  aceq1  8823  zfcndrep  9315  zfcndinf  9319  nfsum1  14268  nfsum  14269  fsum2dlem  14343  nfcprod1  14479  nfcprod  14480  fprod2dlem  14549  brabgaf  28800  cnvoprab  28886  bnj981  30274  bnj1388  30355  bnj1445  30366  bnj1489  30378  bj-axrep2  31977  bj-axrep3  31978  bj-axrep4  31979  pm11.71  37619  upbdrech  38460  stoweidlem57  38950
 Copyright terms: Public domain W3C validator