New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  nfex GIF version

Theorem nfex 1843
 Description: If x is not free in φ, it is not free in ∃yφ. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.)
Hypothesis
Ref Expression
nfal.1 xφ
Assertion
Ref Expression
nfex xyφ

Proof of Theorem nfex
StepHypRef Expression
1 nfal.1 . . . 4 xφ
21nfri 1762 . . 3 (φxφ)
32hbex 1841 . 2 (yφxyφ)
43nfi 1551 1 xyφ
 Colors of variables: wff setvar class Syntax hints:  ∃wex 1541  Ⅎwnf 1544 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746 This theorem depends on definitions:  df-bi 177  df-ex 1542  df-nf 1545 This theorem is referenced by:  19.12  1847  excomimOLD  1858  eeor  1885  eean  1912  cbvex2  2005  nfeu1  2214  moexex  2273  nfel  2497  ceqsex2  2895  copsex2t  4608  copsex2g  4609  mosubopt  4612  nfopab  4627  nfopab2  4629  cbvopab1  4632  cbvopab1s  4634  nfco  4882  dfdmf  4905  dfrnf  4962  fv3  5341  nfoprab2  5547  nfoprab3  5548  nfoprab  5549  cbvoprab1  5567  cbvoprab2  5568  cbvoprab3  5571
 Copyright terms: Public domain W3C validator