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

Theorem nfcri 2744
Description: Consequence of the not-free predicate. (Note that unlike nfcr 2742, 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 2743 . 2 (𝑦𝐴 → ∀𝑥 𝑦𝐴)
32nf5i 2010 1 𝑥 𝑦𝐴
Colors of variables: wff setvar class
Syntax hints:  wnf 1698  wcel 1976  wnfc 2737
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-cleq 2602  df-clel 2605  df-nfc 2739
This theorem is referenced by:  nfnfcALT  2760  sbabel  2778  r2alf  2921  nfrab  3099  cbvralf  3140  cbvrab  3170  nfccdeq  3399  sbcabel  3482  cbvcsb  3503  cbvralcsf  3530  cbvreucsf  3532  cbvrabcsf  3533  dfss2f  3558  nfdif  3692  nfun  3730  nfin  3781  rabasiun  4453  nfiun  4478  nfiin  4479  cbviun  4487  cbviin  4488  cbvdisj  4557  nfdisj  4559  nfmpt  4668  cbvmptf  4670  reusv2lem4  4793  nfxp  5056  opeliunxp  5083  iunxpf  5180  elrnmpt1  5282  nfmpt2  6600  cbvmpt2x  6609  tfis  6923  fmpt2x  7102  nfsum1  14214  nfsum  14215  fsum2dlem  14289  fsumcom2  14293  fsumcom2OLD  14294  nfcprod  14426  cbvprod  14430  fprod2dlem  14495  fprodcom2  14499  fprodcom2OLD  14500  gsum2d2lem  18141  dprd2d2  18212  ptbasfi  21136  restmetu  22126  ovoliunnul  22999  iundisj  23040  iunmbl2  23049  nfitg  23264  limciun  23381  clelsb3f  28510  rmo3f  28525  abrexss  28540  cbviunf  28561  cbvdisjf  28573  disjabrex  28583  disjabrexf  28584  iundisjf  28590  ssrelf  28611  fmptcof2  28645  acunirnmpt2f  28649  iundisjfi  28748  locfinreflem  29041  esum2dlem  29287  oms0  29492  bnj1385  29963  bnj900  30059  bnj1014  30090  bnj1123  30114  bnj1228  30139  bnj1321  30155  bnj1384  30160  bnj1398  30162  bnj1408  30164  bnj1444  30171  bnj1445  30172  bnj1446  30173  bnj1449  30176  bnj1467  30182  bnj1518  30192  bj-nfcf  31908  mptsnunlem  32157  phpreu  32359  poimirlem26  32401  mbfposadd  32423  csbgfi  32901  mpt2bi123f  32937  rababg  36694  ss2iundf  36766  binomcxplemnotnn0  37373  refsumcn  38008  cbvmpt22  38101  cbvmpt21  38102  wessf1ornlem  38162  disjrnmpt2  38166  limcperiod  38492  dvnprodlem1  38633  stoweidlem16  38706  stoweidlem27  38717  stoweidlem28  38718  stoweidlem29  38719  stoweidlem31  38721  stoweidlem34  38724  stoweidlem35  38725  stoweidlem57  38747  stoweidlem59  38749  stirlinglem5  38768  fourierdlem16  38813  fourierdlem21  38818  fourierdlem22  38819  fourierdlem31  38828  fourierdlem48  38844  fourierdlem51  38847  fourierdlem53  38849  fourierdlem80  38876  fourierdlem93  38889  etransclem32  38956  opeliun2xp  41899  cbvmpt2x2  41902
  Copyright terms: Public domain W3C validator