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

Theorem nfcri 2888
Description: Consequence of the not-free predicate. (Note that unlike nfcr 2886, 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 2887 . 2 (𝑦𝐴 → ∀𝑥 𝑦𝐴)
32nf5i 2165 1 𝑥 𝑦𝐴
Colors of variables: wff setvar class
Syntax hints:  wnf 1849  wcel 2131  wnfc 2881
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clel 2748  df-nfc 2883
This theorem is referenced by:  clelsb3f  2898  nfnfcALT  2905  sbabel  2923  r2alf  3068  nfrab  3254  cbvralf  3296  cbvrab  3330  nfccdeq  3566  sbcabel  3650  cbvcsb  3671  cbvralcsf  3698  cbvreucsf  3700  cbvrabcsf  3701  dfss2f  3727  nfdif  3866  nfun  3904  nfin  3955  nfiun  4692  nfiin  4693  cbviun  4701  cbviin  4702  cbvdisj  4774  nfdisj  4776  nfmpt  4890  cbvmptf  4892  reusv2lem4  5013  nfxp  5291  opeliunxp  5319  iunxpf  5418  elrnmpt1  5521  nfmpt2  6881  cbvmpt2x  6890  tfis  7211  fmpt2x  7396  nfsum1  14611  nfsum  14612  fsum2dlem  14692  fsumcom2  14696  fsumcom2OLD  14697  nfcprod  14832  cbvprod  14836  fprod2dlem  14901  fprodcom2  14905  fprodcom2OLD  14906  gsum2d2lem  18564  dprd2d2  18635  ptbasfi  21578  restmetu  22568  ovoliunnul  23467  iundisj  23508  iunmbl2  23517  nfitg  23732  limciun  23849  rmo3f  29635  abrexss  29649  cbviunf  29671  iunin1f  29673  iunxsngf  29674  cbvdisjf  29684  disjabrex  29694  disjabrexf  29695  iundisjf  29701  ssrelf  29726  fmptcof2  29758  acunirnmpt2f  29762  iundisjfi  29856  locfinreflem  30208  esum2dlem  30455  oms0  30660  bnj1385  31202  bnj900  31298  bnj1014  31329  bnj1123  31353  bnj1228  31378  bnj1321  31394  bnj1384  31399  bnj1398  31401  bnj1408  31403  bnj1444  31410  bnj1445  31411  bnj1446  31412  bnj1449  31415  bnj1467  31421  bnj1518  31431  bj-nfcf  33218  mptsnunlem  33488  phpreu  33698  poimirlem26  33740  mbfposadd  33762  csbgfi  34240  mpt2bi123f  34276  rababg  38373  ss2iundf  38445  binomcxplemnotnn0  39049  refsumcn  39680  iunxsngf2  39721  iunssf  39754  cbvmpt22  39768  cbvmpt21  39769  wessf1ornlem  39862  disjrnmpt2  39866  supxrleubrnmptf  40170  limcperiod  40355  limsupequzmptf  40458  dvnprodlem1  40656  stoweidlem16  40728  stoweidlem27  40739  stoweidlem28  40740  stoweidlem29  40741  stoweidlem31  40743  stoweidlem34  40746  stoweidlem35  40747  stoweidlem57  40769  stoweidlem59  40771  stirlinglem5  40790  fourierdlem16  40835  fourierdlem21  40840  fourierdlem22  40841  fourierdlem31  40850  fourierdlem48  40866  fourierdlem51  40869  fourierdlem53  40871  fourierdlem80  40898  fourierdlem93  40911  etransclem32  40978  opeliun2xp  42613  cbvmpt2x2  42616
  Copyright terms: Public domain W3C validator