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

Theorem nfcri 2578
Description: Consequence of the not-free predicate. (Note that unlike nfcr 2576, this does not require  y and  A to be disjoint.) (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypothesis
Ref Expression
nfcri.1  |-  F/_ x A
Assertion
Ref Expression
nfcri  |-  F/ x  y  e.  A
Distinct variable group:    x, y
Allowed substitution hints:    A( x, y)

Proof of Theorem nfcri
StepHypRef Expression
1 nfcri.1 . . 3  |-  F/_ x A
21nfcrii 2577 . 2  |-  ( y  e.  A  ->  A. x  y  e.  A )
32nfi 1671 1  |-  F/ x  y  e.  A
Colors of variables: wff setvar class
Syntax hints:   F/wnf 1664    e. wcel 1869   F/_wnfc 2571
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-ex 1661  df-nf 1665  df-sb 1788  df-cleq 2415  df-clel 2418  df-nfc 2573
This theorem is referenced by:  nfnfcALT  2595  nfeqOLD  2597  nfelOLD  2599  cleqfOLD  2613  sbabel  2617  sbabelOLD  2618  r2alf  2802  r2alfOLD  2803  r2exfOLD  2951  nfrab  3011  cbvralf  3050  cbvrab  3080  nfccdeq  3299  sbcabel  3379  cbvcsb  3402  cbvralcsf  3429  cbvreucsf  3431  cbvrabcsf  3432  dfss2f  3457  nfdif  3588  nfun  3624  nfin  3671  rabasiun  4302  nfiun  4326  nfiin  4327  cbviun  4335  cbviin  4336  cbvdisj  4403  nfdisj  4405  nfmpt  4511  cbvmptf  4513  reusv2lem4  4627  nfxp  4879  opeliunxp  4904  iunxpf  5001  elrnmpt1  5101  nfmpt2  6373  cbvmpt2x  6382  tfis  6694  fmpt2x  6872  nfsum1  13753  nfsum  13754  fsum2dlem  13828  fsumcom2  13832  nfcprod  13962  cbvprod  13966  fprod2dlem  14031  fprodcom2  14035  gsum2d2lem  17602  dprd2d2  17674  ptbasfi  20592  restmetu  21581  ovoliunnul  22456  iundisj  22497  iunmbl2  22506  nfitg  22728  limciun  22845  clelsb3f  28112  rmo3f  28127  abrexss  28143  cbviunf  28169  cbvdisjf  28182  disjabrex  28192  disjabrexf  28193  iundisjf  28199  ssrelf  28221  fmptcof2  28259  acunirnmpt2f  28263  iundisjfi  28376  locfinreflem  28673  oms0  29131  bnj1385  29650  bnj1476  29664  bnj900  29746  bnj1014  29777  bnj1123  29801  bnj1228  29826  bnj1321  29842  bnj1384  29847  bnj1398  29849  bnj1408  29851  bnj1444  29858  bnj1445  29859  bnj1446  29860  bnj1449  29863  bnj1467  29869  bnj1518  29879  bj-nfcf  31494  mptsnunlem  31702  phpreu  31891  poimirlem26  31928  mbfposadd  31950  csbgfi  32332  mpt2bi123f  32368  ss2iundf  36159  binomcxplemnotnn0  36611  refsumcn  37260  wessf1ornlem  37357  disjrnmpt2  37361  limcperiod  37576  dvnprodlem1  37689  stoweidlem16  37744  stoweidlem27  37755  stoweidlem28  37756  stoweidlem29  37757  stoweidlem29OLD  37758  stoweidlem31  37760  stoweidlem34  37763  stoweidlem35  37764  stoweidlem57  37786  stoweidlem59  37788  stirlinglem5  37808  fourierdlem16  37853  fourierdlem21  37858  fourierdlem22  37859  fourierdlem31  37868  fourierdlem31OLD  37869  fourierdlem48  37886  fourierdlem51  37889  fourierdlem53  37891  fourierdlem80  37918  fourierdlem93  37931  etransclem32  37999  opeliun2xp  39508  cbvmpt2x2  39511
  Copyright terms: Public domain W3C validator