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

Theorem nfcri 2598
Description: Consequence of the not-free predicate. (Note that unlike nfcr 2596, 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 2597 . 2  |-  ( y  e.  A  ->  A. x  y  e.  A )
32nfi 1610 1  |-  F/ x  y  e.  A
Colors of variables: wff setvar class
Syntax hints:   F/wnf 1603    e. wcel 1804   F/_wnfc 2591
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1600  df-nf 1604  df-sb 1727  df-cleq 2435  df-clel 2438  df-nfc 2593
This theorem is referenced by:  nfnfcALT  2615  nfeqOLD  2617  nfelOLD  2619  cleqfOLD  2633  sbabel  2636  sbabelOLD  2637  r2alf  2819  r2alfOLD  2820  r2exfOLD  2965  nfrab  3025  cbvralf  3064  cbvrab  3093  nfccdeq  3311  sbcabel  3402  cbvcsb  3425  cbvralcsf  3452  cbvreucsf  3454  cbvrabcsf  3455  dfss2f  3480  nfdif  3610  nfun  3645  nfin  3690  rabasiun  4319  nfiun  4343  nfiin  4344  cbviun  4352  cbviin  4353  cbvdisj  4417  nfdisj  4419  nfmpt  4525  reusv2lem4  4641  nfxp  5016  opeliunxp  5041  iunxpf  5141  elrnmpt1  5241  nfmpt2  6351  cbvmpt2x  6360  tfis  6674  fmpt2x  6851  nfsum1  13494  nfsum  13495  fsum2dlem  13567  fsumcom2  13571  nfcprod  13700  cbvprod  13704  fprod2dlem  13766  fprodcom2  13770  gsum2d2lem  16980  dprd2d2  17072  ptbasfi  20060  restmetu  21068  ovoliunnul  21896  iundisj  21936  iunmbl2  21945  nfitg  22159  limciun  22276  clelsb3f  27357  rmo3f  27372  abrexss  27388  cbvdisjf  27412  disjabrex  27421  disjabrexf  27422  iundisjf  27426  ssrelf  27444  cbvmptf  27472  fmptcof2  27480  iundisjfi  27579  locfinreflem  27821  oms0  28244  mbfposadd  30038  csbgfi  30511  mpt2bi123f  30547  refsumcn  31359  limcperiod  31588  dvnprodlem1  31697  stoweidlem16  31752  stoweidlem27  31763  stoweidlem28  31764  stoweidlem29  31765  stoweidlem31  31767  stoweidlem34  31770  stoweidlem35  31771  stoweidlem57  31793  stoweidlem59  31795  stirlinglem5  31814  fourierdlem16  31859  fourierdlem21  31864  fourierdlem22  31865  fourierdlem31  31874  fourierdlem48  31891  fourierdlem51  31894  fourierdlem53  31896  fourierdlem80  31923  fourierdlem93  31936  opeliun2xp  32790  cbvmpt2x2  32793  bnj1385  33759  bnj1476  33773  bnj900  33855  bnj1014  33886  bnj1123  33910  bnj1228  33935  bnj1321  33951  bnj1384  33956  bnj1398  33958  bnj1408  33960  bnj1444  33967  bnj1445  33968  bnj1446  33969  bnj1449  33972  bnj1467  33978  bnj1518  33988  bj-nfcf  34375
  Copyright terms: Public domain W3C validator