Theorem nfcri 2886

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

Syntax hints:  Ⅎwnf 1790   ∈ wcel 2114  Ⅎwnfc 2879

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787  df-nf 1791  df-clel 2811  df-nfc 2881

This theorem is referenced by:  nfcrii  2891  nfcriiOLD  2892  clelsb3fw  2903  clelsb3f  2904  cleqf  2930  sbabel  2933  r2alf  3134  nfrabw  3288  nfrab  3289  cbvralfw  3335  cbvralfwOLD  3336  cbvralf  3338  cbvrabw  3391  cbvrab  3392  rmo3f  3633  nfccdeq  3677  sbcabel  3769  cbvcsbw  3800  cbvcsb  3801  csbgfi  3810  cbvrabcsfw  3831  cbvralcsf  3832  cbvreucsf  3834  cbvrabcsf  3835  dfss2f  3867  nfdif  4016  nfun  4055  nfin  4107  nfiun  4911  nfiin  4912  nfiung  4913  nfiing  4914  cbviun  4922  cbviin  4923  cbviung  4924  cbviing  4925  iunssf  4930  iunxsngf  4977  cbvdisj  5005  nfdisjw  5007  nfdisj  5008  nfmpt  5127  cbvmptf  5129  cbvmptfg  5130  reusv2lem4  5268  nfxp  5558  opeliunxp  5590  iunxpf  5691  elrnmpt1  5801  nfmpo  7250  cbvmpox  7261  tfis  7588  fmpox  7790  nfsum1  15139  nfsum  15140  nfsumOLD  15141  fsum2dlem  15218  fsumcom2  15222  nfcprod  15357  cbvprod  15361  fprod2dlem  15426  fprodcom2  15430  gsum2d2lem  19212  dprd2d2  19285  ptbasfi  22332  restmetu  23323  ovoliunnul  24259  iundisj  24300  iunmbl2  24309  nfitg  24527  limciun  24646  reuxfrdf  30413  abrexss  30431  cbviunf  30469  iunin1f  30471  cbvdisjf  30484  disjabrex  30495  disjabrexf  30496  iundisjf  30502  ssrelf  30529  2ndresdju  30560  fmptcof2  30569  acunirnmpt2f  30573  iundisjfi  30692  fedgmullem2  31283  locfinreflem  31362  esum2dlem  31630  oms0  31834  bnj1385  32383  bnj900  32480  bnj1014  32512  bnj1123  32537  bnj1228  32562  bnj1321  32578  bnj1384  32583  bnj1398  32585  bnj1408  32587  bnj1444  32594  bnj1445  32595  bnj1446  32596  bnj1449  32599  bnj1467  32605  bnj1518  32615  bj-nfcf  34743  mptsnunlem  35132  phpreu  35384  poimirlem26  35426  mbfposadd  35447  mpobi123f  35943  rababg  40726  ss2iundf  40813  binomcxplemnotnn0  41512  refsumcn  42111  cbvmpo2  42185  cbvmpo1  42186  iinssiin  42216  iinssf  42225  disjrnmpt2  42264  disjinfi  42269  supxrleubrnmptf  42531  limcperiod  42711  limsupequzmptf  42814  dvnprodlem1  43029  stoweidlem16  43099  stoweidlem27  43110  stoweidlem28  43111  stoweidlem29  43112  stoweidlem31  43114  stoweidlem34  43117  stoweidlem35  43118  stoweidlem57  43140  stoweidlem59  43142  stirlinglem5  43161  fourierdlem16  43206  fourierdlem21  43211  fourierdlem22  43212  fourierdlem31  43221  fourierdlem48  43237  fourierdlem51  43240  fourierdlem80  43269  fourierdlem93  43282  etransclem32  43349  opeliun2xp  45202  cbvmpox2  45205