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

Theorem nfcri 2537
Description: Consequence of the not-free predicate. (Note that unlike nfcr 2535, 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 2536 . 2  |-  ( y  e.  A  ->  A. x  y  e.  A )
32nfi 1631 1  |-  F/ x  y  e.  A
Colors of variables: wff setvar class
Syntax hints:   F/wnf 1624    e. wcel 1826   F/_wnfc 2530
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-ex 1621  df-nf 1625  df-sb 1748  df-cleq 2374  df-clel 2377  df-nfc 2532
This theorem is referenced by:  nfnfcALT  2554  nfeqOLD  2556  nfelOLD  2558  cleqfOLD  2572  sbabel  2575  sbabelOLD  2576  r2alf  2758  r2alfOLD  2759  r2exfOLD  2904  nfrab  2964  cbvralf  3003  cbvrab  3032  nfccdeq  3250  sbcabel  3330  cbvcsb  3353  cbvralcsf  3380  cbvreucsf  3382  cbvrabcsf  3383  dfss2f  3408  nfdif  3539  nfun  3574  nfin  3619  rabasiun  4247  nfiun  4271  nfiin  4272  cbviun  4280  cbviin  4281  cbvdisj  4348  nfdisj  4350  nfmpt  4455  reusv2lem4  4569  nfxp  4940  opeliunxp  4965  iunxpf  5064  elrnmpt1  5164  nfmpt2  6265  cbvmpt2x  6274  tfis  6588  fmpt2x  6765  nfsum1  13514  nfsum  13515  fsum2dlem  13587  fsumcom2  13591  nfcprod  13720  cbvprod  13724  fprod2dlem  13786  fprodcom2  13790  gsum2d2lem  17115  dprd2d2  17206  ptbasfi  20167  restmetu  21175  ovoliunnul  22003  iundisj  22043  iunmbl2  22052  nfitg  22266  limciun  22383  clelsb3f  27496  rmo3f  27511  abrexss  27528  cbviunf  27550  cbvdisjf  27563  disjabrex  27572  disjabrexf  27573  iundisjf  27578  ssrelf  27600  cbvmptf  27634  fmptcof2  27643  acunirnmpt2f  27647  iundisjfi  27754  locfinreflem  27997  mbfposadd  30227  csbgfi  30701  mpt2bi123f  30737  binomcxplemnotnn0  31429  refsumcn  31572  limcperiod  31800  dvnprodlem1  31909  stoweidlem16  31964  stoweidlem27  31975  stoweidlem28  31976  stoweidlem29  31977  stoweidlem31  31979  stoweidlem34  31982  stoweidlem35  31983  stoweidlem57  32005  stoweidlem59  32007  stirlinglem5  32026  fourierdlem16  32071  fourierdlem21  32076  fourierdlem22  32077  fourierdlem31  32086  fourierdlem48  32103  fourierdlem51  32106  fourierdlem53  32108  fourierdlem80  32135  fourierdlem93  32148  etransclem32  32215  opeliun2xp  33122  cbvmpt2x2  33125  bnj1385  34238  bnj1476  34252  bnj900  34334  bnj1014  34365  bnj1123  34389  bnj1228  34414  bnj1321  34430  bnj1384  34435  bnj1398  34437  bnj1408  34439  bnj1444  34446  bnj1445  34447  bnj1446  34448  bnj1449  34451  bnj1467  34457  bnj1518  34467  bj-nfcf  34839
  Copyright terms: Public domain W3C validator