Theorem nfcri 2943

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

Syntax hints:  Ⅎwnf 1785   ∈ wcel 2111  Ⅎwnfc 2936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786  df-clel 2870  df-nfc 2938

This theorem is referenced by:  nfcrii  2948  nfcriiOLD  2949  clelsb3fw  2959  clelsb3f  2960  cleqf  2983  sbabel  2986  r2alf  3186  nfrabw  3338  nfrab  3339  cbvralfw  3382  cbvralfwOLD  3383  cbvralf  3385  cbvrabw  3437  cbvrab  3438  rmo3f  3673  nfccdeq  3717  sbcabel  3807  cbvcsbw  3838  cbvcsb  3839  csbgfi  3848  cbvrabcsfw  3869  cbvralcsf  3870  cbvreucsf  3872  cbvrabcsf  3873  dfss2f  3905  nfdif  4053  nfun  4092  nfin  4143  nfiun  4911  nfiin  4912  nfiung  4913  nfiing  4914  cbviun  4923  cbviin  4924  cbviung  4925  cbviing  4926  iunssf  4931  iunxsngf  4977  cbvdisj  5005  nfdisjw  5007  nfdisj  5008  nfmpt  5127  cbvmptf  5129  cbvmptfg  5130  reusv2lem4  5267  nfxp  5552  opeliunxp  5583  iunxpf  5683  elrnmpt1  5794  nfmpo  7215  cbvmpox  7226  tfis  7549  fmpox  7747  nfsum1  15038  nfsum  15039  nfsumOLD  15040  fsum2dlem  15117  fsumcom2  15121  nfcprod  15257  cbvprod  15261  fprod2dlem  15326  fprodcom2  15330  gsum2d2lem  19086  dprd2d2  19159  ptbasfi  22186  restmetu  23177  ovoliunnul  24111  iundisj  24152  iunmbl2  24161  nfitg  24378  limciun  24497  reuxfrdf  30262  abrexss  30280  cbviunf  30319  iunin1f  30321  cbvdisjf  30334  disjabrex  30345  disjabrexf  30346  iundisjf  30352  ssrelf  30379  2ndresdju  30411  fmptcof2  30420  acunirnmpt2f  30424  iundisjfi  30545  fedgmullem2  31114  locfinreflem  31193  esum2dlem  31461  oms0  31665  bnj1385  32214  bnj900  32311  bnj1014  32343  bnj1123  32368  bnj1228  32393  bnj1321  32409  bnj1384  32414  bnj1398  32416  bnj1408  32418  bnj1444  32425  bnj1445  32426  bnj1446  32427  bnj1449  32430  bnj1467  32436  bnj1518  32446  bj-nfcf  34366  mptsnunlem  34755  phpreu  35041  poimirlem26  35083  mbfposadd  35104  mpobi123f  35600  rababg  40273  ss2iundf  40360  binomcxplemnotnn0  41060  refsumcn  41659  cbvmpo2  41733  cbvmpo1  41734  iinssiin  41764  iinssf  41775  disjrnmpt2  41815  disjinfi  41820  supxrleubrnmptf  42090  limcperiod  42270  limsupequzmptf  42373  dvnprodlem1  42588  stoweidlem16  42658  stoweidlem27  42669  stoweidlem28  42670  stoweidlem29  42671  stoweidlem31  42673  stoweidlem34  42676  stoweidlem35  42677  stoweidlem57  42699  stoweidlem59  42701  stirlinglem5  42720  fourierdlem16  42765  fourierdlem21  42770  fourierdlem22  42771  fourierdlem31  42780  fourierdlem48  42796  fourierdlem51  42799  fourierdlem53  42801  fourierdlem80  42828  fourierdlem93  42841  etransclem32  42908  opeliun2xp  44734  cbvmpox2  44737