Theorem nfcri 2886

Description: Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.) Avoid ax-10 2144, ax-11 2160. (Revised by GG, 23-May-2024.) Avoid ax-12 2180 (adopting Wolf Lammen's 13-May-2023 proof). (Revised by SN, 3-Jun-2024.)

Hypothesis

Ref	Expression
nfcri.1	⊢ Ⅎ𝑥𝐴

Assertion

Ref	Expression
nfcri	⊢ Ⅎ𝑥 𝑦 ∈ 𝐴

Distinct variable group:   𝑥,𝑦

Allowed substitution hints:   𝐴(𝑥,𝑦)

Proof of Theorem nfcri

Step	Hyp	Ref	Expression
1		nfcri.1	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcr 2884	. 2 ⊢ (Ⅎ𝑥𝐴 → Ⅎ𝑥 𝑦 ∈ 𝐴)
3	1, 2	ax-mp 5	1 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴

Syntax hints:  Ⅎwnf 1784   ∈ wcel 2111  Ⅎwnfc 2879

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-nf 1785  df-clel 2806  df-nfc 2881

This theorem is referenced by:  nfcrii  2889  clelsb1fw  2898  clelsb1f  2899  cleqf  2923  sbabel  2927  r2alf  3253  cbvralfw  3272  nfralw  3279  cbvralf  3326  nfrmow  3375  nfreuw  3376  cbvrabw  3430  cbvrabwOLD  3431  nfrabw  3432  nfrab  3434  cbvrab  3435  rmo3f  3693  nfccdeq  3737  sbcabel  3829  cbvcsbw  3860  cbvcsb  3861  csbgfi  3870  cbvrabcsfw  3891  cbvralcsf  3892  cbvreucsf  3894  cbvrabcsf  3895  dfssf  3925  nfdif  4079  nfdifOLD  4080  nfun  4120  nfunOLD  4121  nfin  4174  nfinOLD  4175  nfiun  4973  nfiin  4974  nfiung  4975  nfiing  4976  cbviun  4985  cbviin  4986  cbviung  4987  cbviing  4988  iunssf  4993  iunxsngf  5040  cbvdisj  5068  nfdisjw  5070  nfdisj  5071  nfmpt  5189  cbvmptf  5191  cbvmptfg  5192  reusv2lem4  5339  nfxp  5649  opeliunxp  5683  opeliun2xp  5684  iunxpf  5788  elrnmpt1  5900  nfmpo  7428  cbvmpox  7439  tfis  7785  fmpox  7999  nfsum1  15594  nfsum  15595  fsum2dlem  15674  fsumcom2  15678  nfcprod  15813  cbvprod  15817  fprod2dlem  15884  fprodcom2  15888  gsum2d2lem  19883  dprd2d2  19956  ptbasfi  23494  restmetu  24483  ovoliunnul  25433  iundisj  25474  iunmbl2  25483  nfitg  25701  limciun  25820  reuxfrdf  32465  abrexss  32487  cbviunf  32530  iunin1f  32532  cbvdisjf  32546  disjabrex  32557  disjabrexf  32558  iundisjf  32564  ssrelf  32593  2ndresdju  32626  fmptcof2  32634  acunirnmpt2f  32638  iundisjfi  32773  fedgmullem2  33638  irngnzply1  33699  locfinreflem  33848  esum2dlem  34100  oms0  34305  bnj1385  34839  bnj900  34936  bnj1014  34968  bnj1123  34993  bnj1228  35018  bnj1321  35034  bnj1384  35039  bnj1398  35041  bnj1408  35043  bnj1444  35050  bnj1445  35051  bnj1446  35052  bnj1449  35055  bnj1467  35061  bnj1518  35071  bj-nfcf  36956  mptsnunlem  37371  phpreu  37643  poimirlem26  37685  mbfposadd  37706  mpobi123f  38201  rababg  43606  ss2iundf  43691  binomcxplemnotnn0  44388  refsumcn  45066  cbvmpo2  45133  cbvmpo1  45134  iinssiin  45165  iinssf  45174  iindif2f  45196  disjrnmpt2  45224  disjinfi  45228  supxrleubrnmptf  45488  limcperiod  45667  limsupequzmptf  45768  dvnprodlem1  45983  stoweidlem16  46053  stoweidlem27  46064  stoweidlem28  46065  stoweidlem29  46066  stoweidlem31  46068  stoweidlem34  46071  stoweidlem35  46072  stoweidlem57  46094  stoweidlem59  46096  stirlinglem5  46115  fourierdlem16  46160  fourierdlem21  46165  fourierdlem22  46166  fourierdlem31  46175  fourierdlem48  46191  fourierdlem51  46194  fourierdlem80  46223  fourierdlem93  46236  etransclem32  46303  smfsupmpt  46852  smfinfmpt  46856  fsupdm  46879  cbvmpox2  48366  iinfssc  49088  iinfsubc  49089