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

Theorem nfcri 2640
Description: Consequence of the not-free predicate. (Note that unlike nfcr 2638, 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 2639 . 2 (𝑦𝐴 → ∀𝑥 𝑦𝐴)
32nfi 1703 1 𝑥 𝑦𝐴
Colors of variables: wff setvar class
Syntax hints:  wnf 1696  wcel 1937  wnfc 2633
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485
This theorem depends on definitions:  df-bi 192  df-or 379  df-an 380  df-ex 1693  df-nf 1697  df-sb 1829  df-cleq 2498  df-clel 2501  df-nfc 2635
This theorem is referenced by:  nfnfcALT  2656  sbabel  2674  r2alf  2817  nfrab  2993  cbvralf  3034  cbvrab  3064  nfccdeq  3289  sbcabel  3369  cbvcsb  3390  cbvralcsf  3417  cbvreucsf  3419  cbvrabcsf  3420  dfss2f  3445  nfdif  3579  nfun  3617  nfin  3666  rabasiun  4311  nfiun  4335  nfiin  4336  cbviun  4344  cbviin  4345  cbvdisj  4414  nfdisj  4416  nfmpt  4524  cbvmptf  4526  reusv2lem4  4646  nfxp  4907  opeliunxp  4933  iunxpf  5030  elrnmpt1  5132  nfmpt2  6435  cbvmpt2x  6444  tfis  6758  fmpt2x  6936  nfsum1  13916  nfsum  13917  fsum2dlem  13991  fsumcom2  13995  nfcprod  14125  cbvprod  14129  fprod2dlem  14194  fprodcom2  14198  gsum2d2lem  17766  dprd2d2  17837  ptbasfi  20753  restmetu  21743  ovoliunnul  22619  iundisj  22661  iunmbl2  22670  nfitg  22893  limciun  23010  clelsb3f  28277  rmo3f  28292  abrexss  28307  cbviunf  28329  cbvdisjf  28341  disjabrex  28351  disjabrexf  28352  iundisjf  28358  ssrelf  28379  fmptcof2  28416  acunirnmpt2f  28420  iundisjfi  28528  locfinreflem  28822  oms0  29279  bnj1385  29796  bnj1476  29810  bnj900  29892  bnj1014  29923  bnj1123  29947  bnj1228  29972  bnj1321  29988  bnj1384  29993  bnj1398  29995  bnj1408  29997  bnj1444  30004  bnj1445  30005  bnj1446  30006  bnj1449  30009  bnj1467  30015  bnj1518  30025  bj-nfcf  31711  mptsnunlem  31961  phpreu  32162  poimirlem26  32204  mbfposadd  32226  csbgfi  32606  mpt2bi123f  32642  rababg  36418  ss2iundf  36490  binomcxplemnotnn0  37062  refsumcn  37699  wessf1ornlem  37819  disjrnmpt2  37823  limcperiod  38112  dvnprodlem1  38240  stoweidlem16  38312  stoweidlem27  38323  stoweidlem28  38324  stoweidlem29  38325  stoweidlem29OLD  38326  stoweidlem31  38328  stoweidlem34  38331  stoweidlem35  38332  stoweidlem57  38354  stoweidlem59  38356  stirlinglem5  38376  fourierdlem16  38421  fourierdlem21  38426  fourierdlem22  38427  fourierdlem31  38436  fourierdlem31OLD  38437  fourierdlem48  38454  fourierdlem51  38457  fourierdlem53  38459  fourierdlem80  38486  fourierdlem93  38499  etransclem32  38567  opeliun2xp  41304  cbvmpt2x2  41307
  Copyright terms: Public domain W3C validator