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

Theorem nfcri 2907
Description: Consequence of the not-free predicate. (Note that unlike nfcr 2905, 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 2906 . 2 (𝑦𝐴 → ∀𝑥 𝑦𝐴)
32nf5i 2179 1 𝑥 𝑦𝐴
Colors of variables: wff setvar class
Syntax hints:  wnf 1856  wcel 2145  wnfc 2900
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clel 2767  df-nfc 2902
This theorem is referenced by:  clelsb3f  2917  nfnfcALT  2924  sbabel  2942  r2alf  3087  nfrab  3272  cbvralf  3314  cbvrab  3348  nfccdeq  3585  sbcabel  3666  cbvcsb  3687  cbvralcsf  3714  cbvreucsf  3716  cbvrabcsf  3717  dfss2f  3743  nfdif  3882  nfun  3920  nfin  3969  nfiun  4682  nfiin  4683  cbviun  4691  cbviin  4692  cbvdisj  4764  nfdisj  4766  nfmpt  4880  cbvmptf  4882  reusv2lem4  5001  nfxp  5282  opeliunxp  5310  iunxpf  5409  elrnmpt1  5512  nfmpt2  6871  cbvmpt2x  6880  tfis  7201  fmpt2x  7386  nfsum1  14628  nfsum  14629  fsum2dlem  14709  fsumcom2  14713  nfcprod  14848  cbvprod  14852  fprod2dlem  14917  fprodcom2  14921  gsum2d2lem  18579  dprd2d2  18651  ptbasfi  21605  restmetu  22595  ovoliunnul  23495  iundisj  23536  iunmbl2  23545  nfitg  23761  limciun  23878  rmo3f  29674  abrexss  29688  cbviunf  29710  iunin1f  29712  iunxsngf  29713  cbvdisjf  29723  disjabrex  29733  disjabrexf  29734  iundisjf  29740  ssrelf  29765  fmptcof2  29797  acunirnmpt2f  29801  iundisjfi  29895  locfinreflem  30247  esum2dlem  30494  oms0  30699  bnj1385  31241  bnj900  31337  bnj1014  31368  bnj1123  31392  bnj1228  31417  bnj1321  31433  bnj1384  31438  bnj1398  31440  bnj1408  31442  bnj1444  31449  bnj1445  31450  bnj1446  31451  bnj1449  31454  bnj1467  31460  bnj1518  31470  bj-nfcf  33251  mptsnunlem  33522  phpreu  33726  poimirlem26  33768  mbfposadd  33789  csbgfi  34267  mpt2bi123f  34303  rababg  38405  ss2iundf  38477  binomcxplemnotnn0  39081  refsumcn  39711  iunxsngf2  39751  iunssf  39784  cbvmpt22  39798  cbvmpt21  39799  wessf1ornlem  39891  disjrnmpt2  39895  supxrleubrnmptf  40196  limcperiod  40378  limsupequzmptf  40481  dvnprodlem1  40679  stoweidlem16  40750  stoweidlem27  40761  stoweidlem28  40762  stoweidlem29  40763  stoweidlem31  40765  stoweidlem34  40768  stoweidlem35  40769  stoweidlem57  40791  stoweidlem59  40793  stirlinglem5  40812  fourierdlem16  40857  fourierdlem21  40862  fourierdlem22  40863  fourierdlem31  40872  fourierdlem48  40888  fourierdlem51  40891  fourierdlem53  40893  fourierdlem80  40920  fourierdlem93  40933  etransclem32  41000  opeliun2xp  42639  cbvmpt2x2  42642
  Copyright terms: Public domain W3C validator