Theorem nfcri 2894

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

Syntax hints:  Ⅎwnf 1779   ∈ wcel 2105  Ⅎwnfc 2887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-nf 1780  df-clel 2813  df-nfc 2889

This theorem is referenced by:  nfcrii  2897  clelsb1fw  2906  clelsb1f  2907  cleqf  2931  sbabel  2935  sbabelOLD  2936  r2alf  3278  cbvralfw  3301  nfralw  3308  cbvralf  3357  nfrmow  3410  nfreuw  3411  cbvrabw  3470  cbvrabwOLD  3471  nfrabw  3472  nfrabwOLD  3473  nfrab  3475  cbvrab  3476  rmo3f  3742  nfccdeq  3786  sbcabel  3886  cbvcsbw  3917  cbvcsb  3918  csbgfi  3928  cbvrabcsfw  3951  cbvralcsf  3952  cbvreucsf  3954  cbvrabcsf  3955  dfssf  3985  nfdif  4138  nfdifOLD  4139  nfun  4179  nfunOLD  4180  nfin  4231  nfinOLD  4232  nfiun  5027  nfiin  5028  nfiung  5029  nfiing  5030  cbviun  5040  cbviin  5041  cbviung  5042  cbviing  5043  iunssf  5048  iunxsngf  5096  cbvdisj  5124  nfdisjw  5126  nfdisj  5127  nfmpt  5254  cbvmptf  5256  cbvmptfg  5257  reusv2lem4  5406  nfxp  5721  opeliunxp  5755  iunxpf  5861  elrnmpt1  5973  nfmpo  7514  cbvmpox  7525  tfis  7875  fmpox  8090  nfsum1  15722  nfsum  15723  fsum2dlem  15802  fsumcom2  15806  nfcprod  15941  cbvprod  15945  fprod2dlem  16012  fprodcom2  16016  gsum2d2lem  20005  dprd2d2  20078  ptbasfi  23604  restmetu  24598  ovoliunnul  25555  iundisj  25596  iunmbl2  25605  nfitg  25824  limciun  25943  reuxfrdf  32518  abrexss  32539  cbviunf  32575  iunin1f  32577  cbvdisjf  32590  disjabrex  32601  disjabrexf  32602  iundisjf  32608  ssrelf  32634  2ndresdju  32665  fmptcof2  32673  acunirnmpt2f  32677  iundisjfi  32803  fedgmullem2  33657  irngnzply1  33705  locfinreflem  33800  esum2dlem  34072  oms0  34278  bnj1385  34824  bnj900  34921  bnj1014  34953  bnj1123  34978  bnj1228  35003  bnj1321  35019  bnj1384  35024  bnj1398  35026  bnj1408  35028  bnj1444  35035  bnj1445  35036  bnj1446  35037  bnj1449  35040  bnj1467  35046  bnj1518  35056  bj-nfcf  36905  mptsnunlem  37320  phpreu  37590  poimirlem26  37632  mbfposadd  37653  mpobi123f  38148  rababg  43563  ss2iundf  43648  binomcxplemnotnn0  44351  refsumcn  44967  cbvmpo2  45036  cbvmpo1  45037  iinssiin  45068  iinssf  45077  iindif2f  45102  disjrnmpt2  45130  disjinfi  45134  supxrleubrnmptf  45400  limcperiod  45583  limsupequzmptf  45686  dvnprodlem1  45901  stoweidlem16  45971  stoweidlem27  45982  stoweidlem28  45983  stoweidlem29  45984  stoweidlem31  45986  stoweidlem34  45989  stoweidlem35  45990  stoweidlem57  46012  stoweidlem59  46014  stirlinglem5  46033  fourierdlem16  46078  fourierdlem21  46083  fourierdlem22  46084  fourierdlem31  46093  fourierdlem48  46109  fourierdlem51  46112  fourierdlem80  46141  fourierdlem93  46154  etransclem32  46221  smfsupmpt  46770  smfinfmpt  46774  fsupdm  46797  opeliun2xp  48177  cbvmpox2  48180