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

Theorem nfcri 2565
Description: Consequence of the not-free predicate. (Note that unlike nfcr 2563, 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 2564 . 2  |-  ( y  e.  A  ->  A. x  y  e.  A )
32nfi 1560 1  |-  F/ x  y  e.  A
Colors of variables: wff set class
Syntax hints:   F/wnf 1553    e. wcel 1725   F/_wnfc 2558
This theorem is referenced by:  nfnfc  2577  nfeq  2578  nfel  2579  cleqf  2595  sbabel  2597  r2alf  2732  r2exf  2733  nfrab  2881  cbvralf  2918  cbvrab  2946  nfccdeq  3151  sbcabel  3230  cbvcsb  3247  cbvralcsf  3303  cbvreucsf  3305  cbvrabcsf  3306  dfss2f  3331  nfdif  3460  nfun  3495  nfin  3539  nfiun  4111  nfiin  4112  cbviun  4120  cbviin  4121  cbvdisj  4184  nfdisj  4186  nfmpt  4289  reusv2lem4  4719  tfis  4826  nfxp  4896  opeliunxp  4921  iunxpf  5013  elrnmpt1  5111  nfmpt2  6134  cbvmpt2x  6142  fmpt2x  6409  nfsum  12475  cbvsum  12479  fsum2dlem  12544  fsumcom2  12548  gsum2d2lem  15537  dprd2d2  15592  ptbasfi  17603  restmetu  18607  ovoliunnul  19393  iundisj  19432  iunmbl2  19441  nfitg  19656  limciun  19771  clelsb3f  23961  rmo3f  23972  abrexss  23983  cbvdisjf  24005  disjabrex  24014  disjabrexf  24015  iundisjf  24019  cbvmptf  24058  fmptcof2  24066  iundisjfi  24142  nfcprod  25227  cbvprod  25231  fprod2dlem  25294  fprodcom2  25298  refsumcn  27632  stoweidlem16  27696  stoweidlem27  27707  stoweidlem28  27708  stoweidlem29  27709  stoweidlem31  27711  stoweidlem34  27714  stoweidlem35  27715  stoweidlem57  27737  stoweidlem59  27739  stirlinglem5  27758  bnj1385  29105  bnj1476  29119  bnj900  29201  bnj1014  29232  bnj1123  29256  bnj1228  29281  bnj1321  29297  bnj1384  29302  bnj1398  29304  bnj1408  29306  bnj1444  29313  bnj1445  29314  bnj1446  29315  bnj1449  29318  bnj1467  29324  bnj1518  29334
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-cleq 2428  df-clel 2431  df-nfc 2560
  Copyright terms: Public domain W3C validator