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

Theorem nfex 2151
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 2151, hbex 2153. (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 1702 . 2 (∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑)
2 nfex.1 . . . . 5 𝑥𝜑
32nfn 1781 . . . 4 𝑥 ¬ 𝜑
43nfal 2150 . . 3 𝑥𝑦 ¬ 𝜑
54nfn 1781 . 2 𝑥 ¬ ∀𝑦 ¬ 𝜑
61, 5nfxfr 1776 1 𝑥𝑦𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wal 1478  wex 1701  wnf 1705
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-10 2016  ax-11 2031  ax-12 2044
This theorem depends on definitions:  df-bi 197  df-or 385  df-ex 1702  df-nf 1707
This theorem is referenced by:  hbex  2153  nfnf  2155  19.12  2161  eeor  2168  eean  2180  eeeanv  2182  nfeu1  2479  moexex  2540  ceqsex2  3234  nfopab  4690  nfopab2  4692  cbvopab1  4695  cbvopab1s  4697  axrep2  4743  axrep3  4744  axrep4  4745  copsex2t  4927  copsex2g  4928  mosubopt  4942  euotd  4945  nfco  5257  dfdmf  5287  dfrnf  5334  nfdm  5337  fv3  6173  oprabv  6668  nfoprab2  6670  nfoprab3  6671  nfoprab  6672  cbvoprab1  6692  cbvoprab2  6693  cbvoprab3  6696  nfwrecs  7369  ac6sfi  8164  aceq1  8900  zfcndrep  9396  zfcndinf  9400  nfsum1  14370  nfsum  14371  fsum2dlem  14448  nfcprod1  14584  nfcprod  14585  fprod2dlem  14654  brabgaf  29304  cnvoprab  29382  bnj981  30781  bnj1388  30862  bnj1445  30873  bnj1489  30885  bj-axrep2  32485  bj-axrep3  32486  bj-axrep4  32487  pm11.71  38118  upbdrech  39018  stoweidlem57  39611
  Copyright terms: Public domain W3C validator