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

Theorem nfcri 2755
Description: Consequence of the not-free predicate. (Note that unlike nfcr 2753, 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 2754 . 2 (𝑦𝐴 → ∀𝑥 𝑦𝐴)
32nf5i 2021 1 𝑥 𝑦𝐴
Colors of variables: wff setvar class
Syntax hints:  wnf 1705  wcel 1987  wnfc 2748
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-cleq 2614  df-clel 2617  df-nfc 2750
This theorem is referenced by:  nfnfcALT  2771  sbabel  2789  r2alf  2933  nfrab  3112  cbvralf  3153  cbvrab  3184  nfccdeq  3415  sbcabel  3498  cbvcsb  3519  cbvralcsf  3546  cbvreucsf  3548  cbvrabcsf  3549  dfss2f  3574  nfdif  3709  nfun  3747  nfin  3798  rabasiun  4489  nfiun  4514  nfiin  4515  cbviun  4523  cbviin  4524  cbvdisj  4593  nfdisj  4595  nfmpt  4706  cbvmptf  4708  reusv2lem4  4832  nfxp  5102  opeliunxp  5131  iunxpf  5230  elrnmpt1  5334  nfmpt2  6677  cbvmpt2x  6686  tfis  7001  fmpt2x  7181  nfsum1  14354  nfsum  14355  fsum2dlem  14429  fsumcom2  14433  fsumcom2OLD  14434  nfcprod  14566  cbvprod  14570  fprod2dlem  14635  fprodcom2  14639  fprodcom2OLD  14640  gsum2d2lem  18293  dprd2d2  18364  ptbasfi  21294  restmetu  22285  ovoliunnul  23182  iundisj  23223  iunmbl2  23232  nfitg  23447  limciun  23564  clelsb3f  29169  rmo3f  29184  abrexss  29197  cbviunf  29218  iunin1f  29220  iunxsngf  29221  cbvdisjf  29230  disjabrex  29240  disjabrexf  29241  iundisjf  29247  ssrelf  29268  fmptcof2  29299  acunirnmpt2f  29303  iundisjfi  29396  locfinreflem  29689  esum2dlem  29935  oms0  30140  bnj1385  30611  bnj900  30707  bnj1014  30738  bnj1123  30762  bnj1228  30787  bnj1321  30803  bnj1384  30808  bnj1398  30810  bnj1408  30812  bnj1444  30819  bnj1445  30820  bnj1446  30821  bnj1449  30824  bnj1467  30830  bnj1518  30840  bj-nfcf  32567  mptsnunlem  32817  phpreu  33025  poimirlem26  33067  mbfposadd  33089  csbgfi  33567  mpt2bi123f  33603  rababg  37360  ss2iundf  37432  binomcxplemnotnn0  38037  refsumcn  38672  iunxsngf2  38715  iunssf  38748  cbvmpt22  38762  cbvmpt21  38763  wessf1ornlem  38845  disjrnmpt2  38849  limcperiod  39264  limsupequzmptf  39367  dvnprodlem1  39467  stoweidlem16  39540  stoweidlem27  39551  stoweidlem28  39552  stoweidlem29  39553  stoweidlem31  39555  stoweidlem34  39558  stoweidlem35  39559  stoweidlem57  39581  stoweidlem59  39583  stirlinglem5  39602  fourierdlem16  39647  fourierdlem21  39652  fourierdlem22  39653  fourierdlem31  39662  fourierdlem48  39678  fourierdlem51  39681  fourierdlem53  39683  fourierdlem80  39710  fourierdlem93  39723  etransclem32  39790  opeliun2xp  41399  cbvmpt2x2  41402
  Copyright terms: Public domain W3C validator