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

Theorem nfcri 2622
Description: Consequence of the not-free predicate. (Note that unlike nfcr 2620, 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 2621 . 2  |-  ( y  e.  A  ->  A. x  y  e.  A )
32nfi 1606 1  |-  F/ x  y  e.  A
Colors of variables: wff setvar class
Syntax hints:   F/wnf 1599    e. wcel 1767   F/_wnfc 2615
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1597  df-nf 1600  df-sb 1712  df-cleq 2459  df-clel 2462  df-nfc 2617
This theorem is referenced by:  nfnfcALT  2639  nfeqOLD  2641  nfelOLD  2643  cleqf  2656  cleqfOLD  2657  sbabel  2660  sbabelOLD  2661  r2alf  2840  r2alfOLD  2841  r2exfOLD  2984  nfrab  3043  cbvralf  3082  cbvrab  3111  nfccdeq  3329  sbcabel  3420  cbvcsb  3440  cbvralcsf  3467  cbvreucsf  3469  cbvrabcsf  3470  dfss2f  3495  nfdif  3625  nfun  3660  nfin  3705  rabasiun  4329  nfiun  4353  nfiin  4354  cbviun  4362  cbviin  4363  cbvdisj  4427  nfdisj  4429  nfmpt  4535  reusv2lem4  4651  nfxp  5025  opeliunxp  5050  iunxpf  5149  elrnmpt1  5249  nfmpt2  6348  cbvmpt2x  6357  tfis  6667  fmpt2x  6847  fsum2dlem  13544  fsumcom2  13548  gsum2d2lem  16792  dprd2d2  16883  ptbasfi  19817  restmetu  20825  ovoliunnul  21653  iundisj  21693  iunmbl2  21702  nfitg  21916  limciun  22033  clelsb3f  27055  rmo3f  27070  abrexss  27084  cbvdisjf  27107  disjabrex  27116  disjabrexf  27117  iundisjf  27121  cbvmptf  27166  fmptcof2  27174  iundisjfi  27269  nfcprod  28620  cbvprod  28624  fprod2dlem  28687  fprodcom2  28691  csbgfi  30139  mpt2bi123f  30175  refsumcn  30983  stoweidlem16  31316  stoweidlem27  31327  stoweidlem28  31328  stoweidlem29  31329  stoweidlem31  31331  stoweidlem34  31334  stoweidlem35  31335  stoweidlem57  31357  stoweidlem59  31359  stirlinglem5  31378  opeliun2xp  31986  cbvmpt2x2  31989  bnj1385  32970  bnj1476  32984  bnj900  33066  bnj1014  33097  bnj1123  33121  bnj1228  33146  bnj1321  33162  bnj1384  33167  bnj1398  33169  bnj1408  33171  bnj1444  33178  bnj1445  33179  bnj1446  33180  bnj1449  33183  bnj1467  33189  bnj1518  33199
  Copyright terms: Public domain W3C validator