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

Theorem nfcri 2649
Description: Consequence of the not-free predicate. (Note that unlike nfcr 2647, 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 2648 . 2 (𝑦𝐴 → ∀𝑥 𝑦𝐴)
32nfi 1705 1 𝑥 𝑦𝐴
Colors of variables: wff setvar class
Syntax hints:  wnf 1698  wcel 1938  wnfc 2642
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-ex 1695  df-nf 1699  df-sb 1831  df-cleq 2507  df-clel 2510  df-nfc 2644
This theorem is referenced by:  nfnfcALT  2665  sbabel  2683  r2alf  2826  nfrab  3004  cbvralf  3045  cbvrab  3075  nfccdeq  3304  sbcabel  3387  cbvcsb  3408  cbvralcsf  3435  cbvreucsf  3437  cbvrabcsf  3438  dfss2f  3463  nfdif  3597  nfun  3635  nfin  3685  rabasiun  4357  nfiun  4382  nfiin  4383  cbviun  4391  cbviin  4392  cbvdisj  4461  nfdisj  4463  nfmpt  4572  cbvmptf  4574  reusv2lem4  4697  nfxp  4960  opeliunxp  4987  iunxpf  5084  elrnmpt1  5186  nfmpt2  6504  cbvmpt2x  6513  tfis  6827  fmpt2x  7005  nfsum1  14141  nfsum  14142  fsum2dlem  14216  fsumcom2  14220  fsumcom2OLD  14221  nfcprod  14353  cbvprod  14357  fprod2dlem  14422  fprodcom2  14426  fprodcom2OLD  14427  gsum2d2lem  18106  dprd2d2  18177  ptbasfi  21101  restmetu  22091  ovoliunnul  22961  iundisj  23002  iunmbl2  23011  nfitg  23226  limciun  23343  clelsb3f  28496  rmo3f  28511  abrexss  28526  cbviunf  28547  cbvdisjf  28559  disjabrex  28569  disjabrexf  28570  iundisjf  28576  ssrelf  28597  fmptcof2  28631  acunirnmpt2f  28635  iundisjfi  28741  locfinreflem  29035  esum2dlem  29281  oms0  29492  bnj1385  30006  bnj900  30102  bnj1014  30133  bnj1123  30157  bnj1228  30182  bnj1321  30198  bnj1384  30203  bnj1398  30205  bnj1408  30207  bnj1444  30214  bnj1445  30215  bnj1446  30216  bnj1449  30219  bnj1467  30225  bnj1518  30235  bj-nfcf  31947  mptsnunlem  32196  phpreu  32457  poimirlem26  32499  mbfposadd  32521  csbgfi  32999  mpt2bi123f  33035  rababg  36799  ss2iundf  36871  binomcxplemnotnn0  37478  refsumcn  38113  cbvmpt22  38207  cbvmpt21  38208  wessf1ornlem  38268  disjrnmpt2  38272  limcperiod  38598  dvnprodlem1  38743  stoweidlem16  38816  stoweidlem27  38827  stoweidlem28  38828  stoweidlem29  38829  stoweidlem31  38831  stoweidlem34  38834  stoweidlem35  38835  stoweidlem57  38857  stoweidlem59  38859  stirlinglem5  38878  fourierdlem16  38923  fourierdlem21  38928  fourierdlem22  38929  fourierdlem31  38938  fourierdlem31OLD  38939  fourierdlem48  38956  fourierdlem51  38959  fourierdlem53  38961  fourierdlem80  38988  fourierdlem93  39001  etransclem32  39069  opeliun2xp  42013  cbvmpt2x2  42016
  Copyright terms: Public domain W3C validator