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

Theorem nfe1 1732
Description: x is not free in xφ. (Contributed by Mario Carneiro, 11-Aug-2016.)
Assertion
Ref Expression
nfe1 xxφ

Proof of Theorem nfe1
StepHypRef Expression
1 hbe1 1731 . 2 (xφxxφ)
21nfi 1551 1 xxφ
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-6 1729
This theorem depends on definitions:  df-bi 177  df-ex 1542  df-nf 1545
This theorem is referenced by:  19.23tOLD  1819  excomimOLD  1858  nf3  1867  19.38OLD  1874  exan  1882  equs5e  1888  exdistrf  1971  nfmo1  2215  euan  2261  eupicka  2268  mopick2  2271  euor2  2272  moexex  2273  2moex  2275  2euex  2276  2moswap  2279  2eu4  2287  2eu7  2290  2eu8  2291  nfre1  2670  ceqsexg  2970  morex  3020  sbc6g  3071  intab  3956  copsexg  4607  copsex2t  4608  copsex2g  4609  mosubopt  4612  nfopab1  4628  nfopab2  4629  dfid3  4768  imadif  5171  nfoprab1  5546  nfoprab2  5547  nfoprab3  5548
  Copyright terms: Public domain W3C validator