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

Theorem nfcri 2756
Description: Consequence of the not-free predicate. (Note that unlike nfcr 2754, 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 2755 . 2 (𝑦𝐴 → ∀𝑥 𝑦𝐴)
32nf5i 2022 1 𝑥 𝑦𝐴
Colors of variables: wff setvar class
Syntax hints:  wnf 1706  wcel 1988  wnfc 2749
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-cleq 2613  df-clel 2616  df-nfc 2751
This theorem is referenced by:  nfnfcALT  2772  sbabel  2790  r2alf  2935  nfrab  3118  cbvralf  3160  cbvrab  3193  nfccdeq  3427  sbcabel  3510  cbvcsb  3531  cbvralcsf  3558  cbvreucsf  3560  cbvrabcsf  3561  dfss2f  3586  nfdif  3723  nfun  3761  nfin  3812  nfiun  4539  nfiin  4540  cbviun  4548  cbviin  4549  cbvdisj  4621  nfdisj  4623  nfmpt  4737  cbvmptf  4739  reusv2lem4  4863  nfxp  5132  opeliunxp  5160  iunxpf  5259  elrnmpt1  5363  nfmpt2  6709  cbvmpt2x  6718  tfis  7039  fmpt2x  7221  nfsum1  14401  nfsum  14402  fsum2dlem  14482  fsumcom2  14486  fsumcom2OLD  14487  nfcprod  14622  cbvprod  14626  fprod2dlem  14691  fprodcom2  14695  fprodcom2OLD  14696  gsum2d2lem  18353  dprd2d2  18424  ptbasfi  21365  restmetu  22356  ovoliunnul  23256  iundisj  23297  iunmbl2  23306  nfitg  23522  limciun  23639  clelsb3f  29292  rmo3f  29307  abrexss  29322  cbviunf  29344  iunin1f  29346  iunxsngf  29347  cbvdisjf  29357  disjabrex  29367  disjabrexf  29368  iundisjf  29374  ssrelf  29397  fmptcof2  29430  acunirnmpt2f  29434  iundisjfi  29529  locfinreflem  29881  esum2dlem  30128  oms0  30333  bnj1385  30877  bnj900  30973  bnj1014  31004  bnj1123  31028  bnj1228  31053  bnj1321  31069  bnj1384  31074  bnj1398  31076  bnj1408  31078  bnj1444  31085  bnj1445  31086  bnj1446  31087  bnj1449  31090  bnj1467  31096  bnj1518  31106  bj-nfcf  32895  mptsnunlem  33156  phpreu  33364  poimirlem26  33406  mbfposadd  33428  csbgfi  33906  mpt2bi123f  33942  rababg  37698  ss2iundf  37770  binomcxplemnotnn0  38375  refsumcn  39009  iunxsngf2  39050  iunssf  39083  cbvmpt22  39097  cbvmpt21  39098  wessf1ornlem  39187  disjrnmpt2  39191  supxrleubrnmptf  39493  limcperiod  39660  limsupequzmptf  39763  dvnprodlem1  39924  stoweidlem16  39996  stoweidlem27  40007  stoweidlem28  40008  stoweidlem29  40009  stoweidlem31  40011  stoweidlem34  40014  stoweidlem35  40015  stoweidlem57  40037  stoweidlem59  40039  stirlinglem5  40058  fourierdlem16  40103  fourierdlem21  40108  fourierdlem22  40109  fourierdlem31  40118  fourierdlem48  40134  fourierdlem51  40137  fourierdlem53  40139  fourierdlem80  40166  fourierdlem93  40179  etransclem32  40246  opeliun2xp  41876  cbvmpt2x2  41879
  Copyright terms: Public domain W3C validator