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  3730  nfccdeq  3774  sbcabel  3872  cbvcsbw  3903  cbvcsb  3904  csbgfi  3914  cbvrabcsfw  3937  cbvralcsf  3938  cbvreucsf  3940  cbvrabcsf  3941  dfss2f  3972  nfdif  4125  nfun  4165  nfin  4216  nfiun  5027  nfiin  5028  nfiung  5029  nfiing  5030  cbviun  5039  cbviin  5040  cbviung  5041  cbviing  5042  iunssf  5047  iunxsngf  5095  cbvdisj  5123  nfdisjw  5125  nfdisj  5126  nfmpt  5255  cbvmptf  5257  cbvmptfg  5258  reusv2lem4  5399  nfxp  5709  opeliunxp  5742  iunxpf  5847  elrnmpt1  5956  nfmpo  7488  cbvmpox  7499  tfis  7841  fmpox  8050  nfsum1  15633  nfsum  15634  fsum2dlem  15713  fsumcom2  15717  nfcprod  15852  cbvprod  15856  fprod2dlem  15921  fprodcom2  15925  gsum2d2lem  19836  dprd2d2  19909  ptbasfi  23077  restmetu  24071  ovoliunnul  25016  iundisj  25057  iunmbl2  25066  nfitg  25284  limciun  25403  reuxfrdf  31719  abrexss  31737  cbviunf  31775  iunin1f  31777  cbvdisjf  31790  disjabrex  31801  disjabrexf  31802  iundisjf  31808  ssrelf  31832  2ndresdju  31862  fmptcof2  31870  acunirnmpt2f  31874  iundisjfi  31995  fedgmullem2  32704  irngnzply1  32744  locfinreflem  32809  esum2dlem  33079  oms0  33285  bnj1385  33832  bnj900  33929  bnj1014  33961  bnj1123  33986  bnj1228  34011  bnj1321  34027  bnj1384  34032  bnj1398  34034  bnj1408  34036  bnj1444  34043  bnj1445  34044  bnj1446  34045  bnj1449  34048  bnj1467  34054  bnj1518  34064  bj-nfcf  35792  mptsnunlem  36208  phpreu  36461  poimirlem26  36503  mbfposadd  36524  mpobi123f  37019  rababg  42311  ss2iundf  42396  binomcxplemnotnn0  43101  refsumcn  43700  cbvmpo2  43772  cbvmpo1  43773  iinssiin  43804  iinssf  43813  iindif2f  43840  disjrnmpt2  43872  disjinfi  43877  supxrleubrnmptf  44148  limcperiod  44331  limsupequzmptf  44434  dvnprodlem1  44649  stoweidlem16  44719  stoweidlem27  44730  stoweidlem28  44731  stoweidlem29  44732  stoweidlem31  44734  stoweidlem34  44737  stoweidlem35  44738  stoweidlem57  44760  stoweidlem59  44762  stirlinglem5  44781  fourierdlem16  44826  fourierdlem21  44831  fourierdlem22  44832  fourierdlem31  44841  fourierdlem48  44857  fourierdlem51  44860  fourierdlem80  44889  fourierdlem93  44902  etransclem32  44969  smfsupmpt  45518  fsupdm  45545  opeliun2xp  46962  cbvmpox2  46965