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

Theorem nfex 2301
 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 2301, hbex 2303. (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 1854 . 2 (∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑)
2 nfex.1 . . . . 5 𝑥𝜑
32nfn 1933 . . . 4 𝑥 ¬ 𝜑
43nfal 2300 . . 3 𝑥𝑦 ¬ 𝜑
54nfn 1933 . 2 𝑥 ¬ ∀𝑦 ¬ 𝜑
61, 5nfxfr 1928 1 𝑥𝑦𝜑
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3  ∀wal 1630  ∃wex 1853  Ⅎwnf 1857 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-10 2168  ax-11 2183  ax-12 2196 This theorem depends on definitions:  df-bi 197  df-or 384  df-ex 1854  df-nf 1859 This theorem is referenced by:  hbex  2303  nfnf  2305  19.12  2309  eeor  2316  eean  2326  eeeanv  2328  nfeu1  2617  moexex  2679  ceqsex2  3384  nfopab  4870  nfopab2  4872  cbvopab1  4875  cbvopab1s  4877  axrep2  4925  axrep3  4926  axrep4  4927  copsex2t  5105  copsex2g  5106  mosubopt  5120  euotd  5123  nfco  5443  dfdmf  5472  dfrnf  5519  nfdm  5522  fv3  6367  oprabv  6868  nfoprab2  6870  nfoprab3  6871  nfoprab  6872  cbvoprab1  6892  cbvoprab2  6893  cbvoprab3  6896  nfwrecs  7578  ac6sfi  8369  aceq1  9130  zfcndrep  9628  zfcndinf  9632  nfsum1  14619  nfsum  14620  fsum2dlem  14700  nfcprod1  14839  nfcprod  14840  fprod2dlem  14909  brabgaf  29727  cnvoprabOLD  29807  bnj981  31327  bnj1388  31408  bnj1445  31419  bnj1489  31431  nffrecs  32084  bj-axrep2  33095  bj-axrep3  33096  bj-axrep4  33097  pm11.71  39099  upbdrech  40018  stoweidlem57  40777
 Copyright terms: Public domain W3C validator