MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfre1 Unicode version

Theorem nfre1 2918
Description: is not free in . (Contributed by NM, 19-Mar-1997.) (Revised by Mario Carneiro, 7-Oct-2016.)
Assertion
Ref Expression
nfre1

Proof of Theorem nfre1
StepHypRef Expression
1 df-rex 2813 . 2
2 nfe1 1840 . 2
31, 2nfxfr 1645 1
Colors of variables: wff setvar class
Syntax hints:  /\wa 369  E.wex 1612  F/wnf 1616  e.wcel 1818  E.wrex 2808
This theorem is referenced by:  r19.29an  2998  2rmorex  3304  nfiu1  4360  reusv2lem3  4655  eusvobj2  6289  fun11iun  6760  zfregcl  8041  scott0  8325  ac6c4  8882  lbzbi  11199  mreiincl  14993  lss1d  17609  neiptopnei  19633  neitr  19681  bwthOLD  19911  utopsnneiplem  20750  cfilucfilOLD  21072  cfilucfil  21073  mptelee  24198  isch3  26159  atom1d  27272  xrofsup  27582  2sqmo  27637  locfinreflem  27843  esumc  28062  hasheuni  28091  esumcvg  28092  voliune  28201  volfiniune  28202  ddemeas  28208  eulerpartlemgvv  28315  ptrest  30048  indexa  30224  filbcmb  30231  sdclem1  30236  heibor1  30306  suprnmpt  31451  upbdrech  31505  ssfiunibd  31509  iccshift  31558  iooshift  31562  infrglb  31584  islpcn  31645  limsupre  31647  limclner  31657  itgperiod  31780  stoweidlem53  31835  stoweidlem57  31839  fourierdlem48  31937  fourierdlem51  31940  fourierdlem73  31962  fourierdlem81  31970  elaa2  32017  etransclem32  32049  reuan  32185  2reurex  32186  2reu4a  32194  2reu7  32196  2reu8  32197  2zrngagrp  32749  2zrngmmgm  32752  bnj900  33987  bnj1189  34065  bnj1204  34068  bnj1398  34090  bnj1444  34099  bnj1445  34100  bnj1446  34101  bnj1447  34102  bnj1467  34110  bnj1518  34120  bnj1519  34121  dihglblem5  37025
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-10 1837
This theorem depends on definitions:  df-bi 185  df-ex 1613  df-nf 1617  df-rex 2813
  Copyright terms: Public domain W3C validator