Theorem nfcri 2891

Description: Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.) Avoid ax-10 2138, ax-11 2155. (Revised by Gino Giotto, 23-May-2024.) Avoid ax-12 2172 (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 2889	. 2 ⊢ (Ⅎ𝑥𝐴 → Ⅎ𝑥 𝑦 ∈ 𝐴)
3	1, 2	ax-mp 5	1 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴

Syntax hints:  Ⅎwnf 1786   ∈ wcel 2107  Ⅎwnfc 2884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-nf 1787  df-clel 2811  df-nfc 2886

This theorem is referenced by:  nfcrii  2896  nfcriiOLD  2897  clelsb1fw  2908  clelsb1f  2909  cleqf  2935  sbabel  2939  sbabelOLD  2940  r2alf  3279  cbvralfw  3302  nfralw  3309  cbvralfwOLD  3321  cbvralf  3357  nfrmow  3410  nfreuw  3411  cbvrabw  3468  nfrabw  3469  nfrabwOLD  3470  nfrab  3473  cbvrab  3474  rmo3f  3731  nfccdeq  3775  sbcabel  3873  cbvcsbw  3904  cbvcsb  3905  csbgfi  3915  cbvrabcsfw  3938  cbvralcsf  3939  cbvreucsf  3941  cbvrabcsf  3942  dfss2f  3973  nfdif  4126  nfun  4166  nfin  4217  nfiun  5028  nfiin  5029  nfiung  5030  nfiing  5031  cbviun  5040  cbviin  5041  cbviung  5042  cbviing  5043  iunssf  5048  iunxsngf  5096  cbvdisj  5124  nfdisjw  5126  nfdisj  5127  nfmpt  5256  cbvmptf  5258  cbvmptfg  5259  reusv2lem4  5400  nfxp  5710  opeliunxp  5744  iunxpf  5849  elrnmpt1  5958  nfmpo  7491  cbvmpox  7502  tfis  7844  fmpox  8053  nfsum1  15636  nfsum  15637  fsum2dlem  15716  fsumcom2  15720  nfcprod  15855  cbvprod  15859  fprod2dlem  15924  fprodcom2  15928  gsum2d2lem  19841  dprd2d2  19914  ptbasfi  23085  restmetu  24079  ovoliunnul  25024  iundisj  25065  iunmbl2  25074  nfitg  25292  limciun  25411  reuxfrdf  31731  abrexss  31749  cbviunf  31787  iunin1f  31789  cbvdisjf  31802  disjabrex  31813  disjabrexf  31814  iundisjf  31820  ssrelf  31844  2ndresdju  31874  fmptcof2  31882  acunirnmpt2f  31886  iundisjfi  32007  fedgmullem2  32715  irngnzply1  32755  locfinreflem  32820  esum2dlem  33090  oms0  33296  bnj1385  33843  bnj900  33940  bnj1014  33972  bnj1123  33997  bnj1228  34022  bnj1321  34038  bnj1384  34043  bnj1398  34045  bnj1408  34047  bnj1444  34054  bnj1445  34055  bnj1446  34056  bnj1449  34059  bnj1467  34065  bnj1518  34075  bj-nfcf  35803  mptsnunlem  36219  phpreu  36472  poimirlem26  36514  mbfposadd  36535  mpobi123f  37030  rababg  42325  ss2iundf  42410  binomcxplemnotnn0  43115  refsumcn  43714  cbvmpo2  43786  cbvmpo1  43787  iinssiin  43818  iinssf  43827  iindif2f  43854  disjrnmpt2  43886  disjinfi  43891  supxrleubrnmptf  44161  limcperiod  44344  limsupequzmptf  44447  dvnprodlem1  44662  stoweidlem16  44732  stoweidlem27  44743  stoweidlem28  44744  stoweidlem29  44745  stoweidlem31  44747  stoweidlem34  44750  stoweidlem35  44751  stoweidlem57  44773  stoweidlem59  44775  stirlinglem5  44794  fourierdlem16  44839  fourierdlem21  44844  fourierdlem22  44845  fourierdlem31  44854  fourierdlem48  44870  fourierdlem51  44873  fourierdlem80  44902  fourierdlem93  44915  etransclem32  44982  smfsupmpt  45531  fsupdm  45558  opeliun2xp  47008  cbvmpox2  47011