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

Theorem nfex 2318
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 2318, hbex 2319. (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 1783 . 2 (∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑)
2 nfex.1 . . . . 5 𝑥𝜑
32nfn 1861 . . . 4 𝑥 ¬ 𝜑
43nfal 2317 . . 3 𝑥𝑦 ¬ 𝜑
54nfn 1861 . 2 𝑥 ¬ ∀𝑦 ¬ 𝜑
61, 5nfxfr 1856 1 𝑥𝑦𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wal 1540  wex 1782  wnf 1786
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-10 2138  ax-11 2155  ax-12 2172
This theorem depends on definitions:  df-bi 206  df-or 847  df-ex 1783  df-nf 1787
This theorem is referenced by:  hbex  2319  nfnf  2320  19.12  2321  eeorOLD  2331  eean  2345  eeeanv  2347  nfmo1  2556  nfeu1  2587  moexexlem  2627  r19.12  3300  r19.12OLD  3301  ceqsex2  3501  nfopab2  5181  cbvopab1  5185  cbvopab1g  5186  cbvopab1s  5188  axrep2  5250  axrep3  5251  axrep4  5252  copsex2t  5454  copsex2gOLD  5456  mosubopt  5472  euotd  5475  nfco  5826  dfdmf  5857  dfrnf  5910  nfdm  5911  fv3  6865  oprabv  7422  nfoprab2  7424  nfoprab3  7425  nfoprab  7426  cbvoprab1  7449  cbvoprab2  7450  cbvoprab3  7453  nffrecs  8219  nfwrecsOLD  8253  ac6sfi  9238  aceq1  10060  zfcndrep  10557  zfcndinf  10561  nfsum1  15581  nfsum  15582  nfsumOLD  15583  fsum2dlem  15662  nfcprod1  15800  nfcprod  15801  fprod2dlem  15870  brabgaf  31569  2ndresdju  31607  cnvoprabOLD  31679  bnj981  33602  bnj1388  33685  bnj1445  33696  bnj1489  33708  fineqvrep  33736  bj-opabco  35688  pm11.71  42751  upbdrech  43613  stoweidlem57  44372  or2expropbi  45342  ich2exprop  45737  ichnreuop  45738  ichreuopeq  45739  reuopreuprim  45792  pgind  47236
  Copyright terms: Public domain W3C validator