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

Theorem nfcri 2612
Description: Consequence of the not-free predicate. (Note that unlike nfcr 2610, this does not require and to be disjoint.) (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypothesis
Ref Expression
nfcri.1
Assertion
Ref Expression
nfcri
Distinct variable group:   ,

Proof of Theorem nfcri
StepHypRef Expression
1 nfcri.1 . . 3
21nfcrii 2611 . 2
32nfi 1623 1
Colors of variables: wff setvar class
Syntax hints:  F/wnf 1616  e.wcel 1818  F/_wnfc 2605
This theorem is referenced by:  nfnfcALT  2629  nfeqOLD  2631  nfelOLD  2633  cleqfOLD  2647  sbabel  2650  sbabelOLD  2651  r2alf  2833  r2alfOLD  2834  r2exfOLD  2979  nfrab  3039  cbvralf  3078  cbvrab  3107  nfccdeq  3325  sbcabel  3416  cbvcsb  3439  cbvralcsf  3466  cbvreucsf  3468  cbvrabcsf  3469  dfss2f  3494  nfdif  3624  nfun  3659  nfin  3704  rabasiun  4334  nfiun  4358  nfiin  4359  cbviun  4367  cbviin  4368  cbvdisj  4432  nfdisj  4434  nfmpt  4540  reusv2lem4  4656  nfxp  5031  opeliunxp  5056  iunxpf  5156  elrnmpt1  5256  nfmpt2  6366  cbvmpt2x  6375  tfis  6689  fmpt2x  6866  nfsum1  13512  nfsum  13513  fsum2dlem  13585  fsumcom2  13589  nfcprod  13718  cbvprod  13722  fprod2dlem  13784  fprodcom2  13788  gsum2d2lem  17001  dprd2d2  17093  ptbasfi  20082  restmetu  21090  ovoliunnul  21918  iundisj  21958  iunmbl2  21967  nfitg  22181  limciun  22298  clelsb3f  27379  rmo3f  27394  abrexss  27410  cbvdisjf  27434  disjabrex  27443  disjabrexf  27444  iundisjf  27448  ssrelf  27466  cbvmptf  27494  fmptcof2  27502  iundisjfi  27601  locfinreflem  27843  oms0  28266  mbfposadd  30062  csbgfi  30535  mpt2bi123f  30571  binomcxplemnotnn0  31261  refsumcn  31405  limcperiod  31634  dvnprodlem1  31743  stoweidlem16  31798  stoweidlem27  31809  stoweidlem28  31810  stoweidlem29  31811  stoweidlem31  31813  stoweidlem34  31816  stoweidlem35  31817  stoweidlem57  31839  stoweidlem59  31841  stirlinglem5  31860  fourierdlem16  31905  fourierdlem21  31910  fourierdlem22  31911  fourierdlem31  31920  fourierdlem48  31937  fourierdlem51  31940  fourierdlem53  31942  fourierdlem80  31969  fourierdlem93  31982  etransclem32  32049  opeliun2xp  32922  cbvmpt2x2  32925  bnj1385  33891  bnj1476  33905  bnj900  33987  bnj1014  34018  bnj1123  34042  bnj1228  34067  bnj1321  34083  bnj1384  34088  bnj1398  34090  bnj1408  34092  bnj1444  34099  bnj1445  34100  bnj1446  34101  bnj1449  34104  bnj1467  34110  bnj1518  34120  bj-nfcf  34492
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-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1613  df-nf 1617  df-sb 1740  df-cleq 2449  df-clel 2452  df-nfc 2607
  Copyright terms: Public domain W3C validator