Theorem nfcri 2894

Description: Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.) Avoid ax-10 2137, ax-11 2154. (Revised by Gino Giotto, 23-May-2024.) Avoid ax-12 2171 (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 1786   ∈ wcel 2106  Ⅎwnfc 2887

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 1913  ax-6 1971  ax-7 2011  ax-8 2108

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-nf 1787  df-clel 2816  df-nfc 2889

This theorem is referenced by:  nfcrii  2899  nfcriiOLD  2900  clelsb1fw  2911  clelsb1f  2912  cleqf  2938  sbabel  2941  sbabelOLD  2942  r2alf  3147  nfralw  3151  nfrmow  3304  nfreuw  3305  nfrabw  3318  nfrabwOLD  3319  nfrab  3320  cbvralfw  3368  cbvralfwOLD  3369  cbvralf  3371  cbvrabw  3424  cbvrab  3425  rmo3f  3669  nfccdeq  3713  sbcabel  3811  cbvcsbw  3842  cbvcsb  3843  csbgfi  3853  cbvrabcsfw  3876  cbvralcsf  3877  cbvreucsf  3879  cbvrabcsf  3880  dfss2f  3911  nfdif  4060  nfun  4099  nfin  4150  nfiun  4954  nfiin  4955  nfiung  4956  nfiing  4957  cbviun  4966  cbviin  4967  cbviung  4968  cbviing  4969  iunssf  4974  iunxsngf  5021  cbvdisj  5049  nfdisjw  5051  nfdisj  5052  nfmpt  5181  cbvmptf  5183  cbvmptfg  5184  reusv2lem4  5324  nfxp  5622  opeliunxp  5654  iunxpf  5757  elrnmpt1  5867  nfmpo  7357  cbvmpox  7368  tfis  7701  fmpox  7907  nfsum1  15401  nfsum  15402  nfsumOLD  15403  fsum2dlem  15482  fsumcom2  15486  nfcprod  15621  cbvprod  15625  fprod2dlem  15690  fprodcom2  15694  gsum2d2lem  19574  dprd2d2  19647  ptbasfi  22732  restmetu  23726  ovoliunnul  24671  iundisj  24712  iunmbl2  24721  nfitg  24939  limciun  25058  reuxfrdf  30839  abrexss  30857  cbviunf  30895  iunin1f  30897  cbvdisjf  30910  disjabrex  30921  disjabrexf  30922  iundisjf  30928  ssrelf  30955  2ndresdju  30986  fmptcof2  30994  acunirnmpt2f  30998  iundisjfi  31117  fedgmullem2  31711  locfinreflem  31790  esum2dlem  32060  oms0  32264  bnj1385  32812  bnj900  32909  bnj1014  32941  bnj1123  32966  bnj1228  32991  bnj1321  33007  bnj1384  33012  bnj1398  33014  bnj1408  33016  bnj1444  33023  bnj1445  33024  bnj1446  33025  bnj1449  33028  bnj1467  33034  bnj1518  33044  bj-nfcf  35111  mptsnunlem  35509  phpreu  35761  poimirlem26  35803  mbfposadd  35824  mpobi123f  36320  rababg  41181  ss2iundf  41267  binomcxplemnotnn0  41974  refsumcn  42573  cbvmpo2  42647  cbvmpo1  42648  iinssiin  42678  iinssf  42687  disjrnmpt2  42726  disjinfi  42731  supxrleubrnmptf  42991  limcperiod  43169  limsupequzmptf  43272  dvnprodlem1  43487  stoweidlem16  43557  stoweidlem27  43568  stoweidlem28  43569  stoweidlem29  43570  stoweidlem31  43572  stoweidlem34  43575  stoweidlem35  43576  stoweidlem57  43598  stoweidlem59  43600  stirlinglem5  43619  fourierdlem16  43664  fourierdlem21  43669  fourierdlem22  43670  fourierdlem31  43679  fourierdlem48  43695  fourierdlem51  43698  fourierdlem80  43727  fourierdlem93  43740  etransclem32  43807  smfsupmpt  44348  opeliun2xp  45668  cbvmpox2  45671