Theorem nfcri 2890

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

Syntax hints:  Ⅎwnf 1784   ∈ wcel 2113  Ⅎwnfc 2883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-nf 1785  df-clel 2811  df-nfc 2885

This theorem is referenced by:  nfcrii  2893  clelsb1fw  2902  clelsb1f  2903  cleqf  2927  sbabel  2931  r2alf  3257  cbvralfw  3276  nfralw  3283  cbvralf  3330  nfrmow  3379  nfreuw  3380  cbvrabw  3434  cbvrabwOLD  3435  nfrabw  3436  nfrab  3438  cbvrab  3439  rmo3f  3692  nfccdeq  3736  sbcabel  3828  cbvcsbw  3859  cbvcsb  3860  csbgfi  3869  cbvrabcsfw  3890  cbvralcsf  3891  cbvreucsf  3893  cbvrabcsf  3894  dfssf  3924  nfdif  4081  nfdifOLD  4082  nfun  4122  nfunOLD  4123  nfin  4176  nfinOLD  4177  nfiun  4978  nfiin  4979  nfiung  4980  nfiing  4981  cbviun  4990  cbviin  4991  cbviung  4992  cbviing  4993  iunssf  4998  iunssfOLD  4999  iunxsngf  5047  cbvdisj  5075  nfdisjw  5077  nfdisj  5078  nfmpt  5196  cbvmptf  5198  cbvmptfg  5199  reusv2lem4  5346  nfxp  5657  opeliunxp  5691  opeliun2xp  5692  iunxpf  5797  elrnmpt1  5909  nfmpo  7440  cbvmpox  7451  tfis  7797  fmpox  8011  nfsum1  15613  nfsum  15614  fsum2dlem  15693  fsumcom2  15697  nfcprod  15832  cbvprod  15836  fprod2dlem  15903  fprodcom2  15907  gsum2d2lem  19902  dprd2d2  19975  ptbasfi  23525  restmetu  24514  ovoliunnul  25464  iundisj  25505  iunmbl2  25514  nfitg  25732  limciun  25851  reuxfrdf  32565  abrexss  32587  cbviunf  32630  iunin1f  32632  cbvdisjf  32646  disjabrex  32657  disjabrexf  32658  iundisjf  32664  ssrelf  32693  2ndresdju  32727  fmptcof2  32735  acunirnmpt2f  32739  iundisjfi  32876  fedgmullem2  33787  irngnzply1  33848  locfinreflem  33997  esum2dlem  34249  oms0  34454  bnj1385  34988  bnj900  35085  bnj1014  35117  bnj1123  35142  bnj1228  35167  bnj1321  35183  bnj1384  35188  bnj1398  35190  bnj1408  35192  bnj1444  35199  bnj1445  35200  bnj1446  35201  bnj1449  35204  bnj1467  35210  bnj1518  35220  bj-nfcf  37124  mptsnunlem  37539  phpreu  37801  poimirlem26  37843  mbfposadd  37864  mpobi123f  38359  rababg  43811  ss2iundf  43896  binomcxplemnotnn0  44593  refsumcn  45271  cbvmpo2  45337  cbvmpo1  45338  iinssiin  45369  iinssf  45378  iindif2f  45400  disjrnmpt2  45428  disjinfi  45432  supxrleubrnmptf  45691  limcperiod  45870  limsupequzmptf  45971  dvnprodlem1  46186  stoweidlem16  46256  stoweidlem27  46267  stoweidlem28  46268  stoweidlem29  46269  stoweidlem31  46271  stoweidlem34  46274  stoweidlem35  46275  stoweidlem57  46297  stoweidlem59  46299  stirlinglem5  46318  fourierdlem16  46363  fourierdlem21  46368  fourierdlem22  46369  fourierdlem31  46378  fourierdlem48  46394  fourierdlem51  46397  fourierdlem80  46426  fourierdlem93  46439  etransclem32  46506  smfsupmpt  47055  smfinfmpt  47059  fsupdm  47082  cbvmpox2  48578  iinfssc  49298  iinfsubc  49299