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

Theorem nfcri 2745
Description: Consequence of the not-free predicate. (Note that unlike nfcr 2743, this does not require 𝑦 and 𝐴 to be disjoint.) (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypothesis
Ref Expression
nfcri.1 𝑥𝐴
Assertion
Ref Expression
nfcri 𝑥 𝑦𝐴
Distinct variable group:   𝑥,𝑦
Allowed substitution hints:   𝐴(𝑥,𝑦)

Proof of Theorem nfcri
StepHypRef Expression
1 nfcri.1 . . 3 𝑥𝐴
21nfcrii 2744 . 2 (𝑦𝐴 → ∀𝑥 𝑦𝐴)
32nf5i 2011 1 𝑥 𝑦𝐴
Colors of variables: wff setvar class
Syntax hints:  wnf 1699  wcel 1977  wnfc 2738
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-cleq 2603  df-clel 2606  df-nfc 2740
This theorem is referenced by:  nfnfcALT  2761  sbabel  2779  r2alf  2922  nfrab  3100  cbvralf  3141  cbvrab  3171  nfccdeq  3400  sbcabel  3483  cbvcsb  3504  cbvralcsf  3531  cbvreucsf  3533  cbvrabcsf  3534  dfss2f  3559  nfdif  3693  nfun  3731  nfin  3782  rabasiun  4459  nfiun  4484  nfiin  4485  cbviun  4493  cbviin  4494  cbvdisj  4563  nfdisj  4565  nfmpt  4674  cbvmptf  4676  reusv2lem4  4798  nfxp  5066  opeliunxp  5093  iunxpf  5192  elrnmpt1  5295  nfmpt2  6622  cbvmpt2x  6631  tfis  6946  fmpt2x  7125  nfsum1  14268  nfsum  14269  fsum2dlem  14343  fsumcom2  14347  fsumcom2OLD  14348  nfcprod  14480  cbvprod  14484  fprod2dlem  14549  fprodcom2  14553  fprodcom2OLD  14554  gsum2d2lem  18195  dprd2d2  18266  ptbasfi  21194  restmetu  22185  ovoliunnul  23082  iundisj  23123  iunmbl2  23132  nfitg  23347  limciun  23464  clelsb3f  28704  rmo3f  28719  abrexss  28734  cbviunf  28755  cbvdisjf  28767  disjabrex  28777  disjabrexf  28778  iundisjf  28784  ssrelf  28805  fmptcof2  28839  acunirnmpt2f  28843  iundisjfi  28942  locfinreflem  29235  esum2dlem  29481  oms0  29686  bnj1385  30157  bnj900  30253  bnj1014  30284  bnj1123  30308  bnj1228  30333  bnj1321  30349  bnj1384  30354  bnj1398  30356  bnj1408  30358  bnj1444  30365  bnj1445  30366  bnj1446  30367  bnj1449  30370  bnj1467  30376  bnj1518  30386  bj-nfcf  32112  mptsnunlem  32361  phpreu  32563  poimirlem26  32605  mbfposadd  32627  csbgfi  33105  mpt2bi123f  33141  rababg  36898  ss2iundf  36970  binomcxplemnotnn0  37577  refsumcn  38212  cbvmpt22  38305  cbvmpt21  38306  wessf1ornlem  38366  disjrnmpt2  38370  limcperiod  38695  dvnprodlem1  38836  stoweidlem16  38909  stoweidlem27  38920  stoweidlem28  38921  stoweidlem29  38922  stoweidlem31  38924  stoweidlem34  38927  stoweidlem35  38928  stoweidlem57  38950  stoweidlem59  38952  stirlinglem5  38971  fourierdlem16  39016  fourierdlem21  39021  fourierdlem22  39022  fourierdlem31  39031  fourierdlem48  39047  fourierdlem51  39050  fourierdlem53  39052  fourierdlem80  39079  fourierdlem93  39092  etransclem32  39159  opeliun2xp  41904  cbvmpt2x2  41907
  Copyright terms: Public domain W3C validator