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

Theorem nfcri 2606
Description: Consequence of the not-free predicate. (Note that unlike nfcr 2604, 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 2605 . 2  |-  ( y  e.  A  ->  A. x  y  e.  A )
32nfi 1682 1  |-  F/ x  y  e.  A
Colors of variables: wff setvar class
Syntax hints:   F/wnf 1675    e. wcel 1904   F/_wnfc 2599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-ex 1672  df-nf 1676  df-sb 1806  df-cleq 2464  df-clel 2467  df-nfc 2601
This theorem is referenced by:  nfnfcALT  2622  sbabel  2640  r2alf  2782  nfrab  2958  cbvralf  2999  cbvrab  3029  nfccdeq  3253  sbcabel  3333  cbvcsb  3354  cbvralcsf  3381  cbvreucsf  3383  cbvrabcsf  3384  dfss2f  3409  nfdif  3543  nfun  3581  nfin  3630  rabasiun  4273  nfiun  4297  nfiin  4298  cbviun  4306  cbviin  4307  cbvdisj  4376  nfdisj  4378  nfmpt  4484  cbvmptf  4486  reusv2lem4  4605  nfxp  4866  opeliunxp  4891  iunxpf  4988  elrnmpt1  5089  nfmpt2  6379  cbvmpt2x  6388  tfis  6700  fmpt2x  6878  nfsum1  13833  nfsum  13834  fsum2dlem  13908  fsumcom2  13912  nfcprod  14042  cbvprod  14046  fprod2dlem  14111  fprodcom2  14115  gsum2d2lem  17683  dprd2d2  17755  ptbasfi  20673  restmetu  21663  ovoliunnul  22538  iundisj  22580  iunmbl2  22589  nfitg  22811  limciun  22928  clelsb3f  28195  rmo3f  28210  abrexss  28225  cbviunf  28247  cbvdisjf  28259  disjabrex  28269  disjabrexf  28270  iundisjf  28276  ssrelf  28297  fmptcof2  28334  acunirnmpt2f  28338  iundisjfi  28447  locfinreflem  28741  oms0  29198  bnj1385  29716  bnj1476  29730  bnj900  29812  bnj1014  29843  bnj1123  29867  bnj1228  29892  bnj1321  29908  bnj1384  29913  bnj1398  29915  bnj1408  29917  bnj1444  29924  bnj1445  29925  bnj1446  29926  bnj1449  29929  bnj1467  29935  bnj1518  29945  bj-nfcf  31595  mptsnunlem  31810  phpreu  31993  poimirlem26  32030  mbfposadd  32052  csbgfi  32434  mpt2bi123f  32470  rababg  36250  ss2iundf  36322  binomcxplemnotnn0  36775  refsumcn  37414  wessf1ornlem  37530  disjrnmpt2  37534  limcperiod  37805  dvnprodlem1  37918  stoweidlem16  37988  stoweidlem27  37999  stoweidlem28  38000  stoweidlem29  38001  stoweidlem29OLD  38002  stoweidlem31  38004  stoweidlem34  38007  stoweidlem35  38008  stoweidlem57  38030  stoweidlem59  38032  stirlinglem5  38052  fourierdlem16  38097  fourierdlem21  38102  fourierdlem22  38103  fourierdlem31  38112  fourierdlem31OLD  38113  fourierdlem48  38130  fourierdlem51  38133  fourierdlem53  38135  fourierdlem80  38162  fourierdlem93  38175  etransclem32  38243  opeliun2xp  40622  cbvmpt2x2  40625
  Copyright terms: Public domain W3C validator