Theorem nfcri 2883

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

Syntax hints:  Ⅎwnf 1783   ∈ wcel 2109  Ⅎwnfc 2876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-nf 1784  df-clel 2803  df-nfc 2878

This theorem is referenced by:  nfcrii  2886  clelsb1fw  2895  clelsb1f  2896  cleqf  2920  sbabel  2924  r2alf  3250  cbvralfw  3270  nfralw  3277  cbvralf  3325  nfrmow  3376  nfreuw  3377  cbvrabw  3432  cbvrabwOLD  3433  nfrabw  3434  nfrab  3436  cbvrab  3437  rmo3f  3696  nfccdeq  3740  sbcabel  3832  cbvcsbw  3863  cbvcsb  3864  csbgfi  3873  cbvrabcsfw  3894  cbvralcsf  3895  cbvreucsf  3897  cbvrabcsf  3898  dfssf  3928  nfdif  4082  nfdifOLD  4083  nfun  4123  nfunOLD  4124  nfin  4177  nfinOLD  4178  nfiun  4976  nfiin  4977  nfiung  4978  nfiing  4979  cbviun  4988  cbviin  4989  cbviung  4990  cbviing  4991  iunssf  4996  iunxsngf  5044  cbvdisj  5072  nfdisjw  5074  nfdisj  5075  nfmpt  5193  cbvmptf  5195  cbvmptfg  5196  reusv2lem4  5343  nfxp  5656  opeliunxp  5690  opeliun2xp  5691  iunxpf  5795  elrnmpt1  5906  nfmpo  7435  cbvmpox  7446  tfis  7795  fmpox  8009  nfsum1  15615  nfsum  15616  fsum2dlem  15695  fsumcom2  15699  nfcprod  15834  cbvprod  15838  fprod2dlem  15905  fprodcom2  15909  gsum2d2lem  19870  dprd2d2  19943  ptbasfi  23484  restmetu  24474  ovoliunnul  25424  iundisj  25465  iunmbl2  25474  nfitg  25692  limciun  25811  reuxfrdf  32453  abrexss  32474  cbviunf  32517  iunin1f  32519  cbvdisjf  32533  disjabrex  32544  disjabrexf  32545  iundisjf  32551  ssrelf  32576  2ndresdju  32606  fmptcof2  32614  acunirnmpt2f  32618  iundisjfi  32752  fedgmullem2  33602  irngnzply1  33662  locfinreflem  33806  esum2dlem  34058  oms0  34264  bnj1385  34798  bnj900  34895  bnj1014  34927  bnj1123  34952  bnj1228  34977  bnj1321  34993  bnj1384  34998  bnj1398  35000  bnj1408  35002  bnj1444  35009  bnj1445  35010  bnj1446  35011  bnj1449  35014  bnj1467  35020  bnj1518  35030  bj-nfcf  36896  mptsnunlem  37311  phpreu  37583  poimirlem26  37625  mbfposadd  37646  mpobi123f  38141  rababg  43547  ss2iundf  43632  binomcxplemnotnn0  44329  refsumcn  45008  cbvmpo2  45075  cbvmpo1  45076  iinssiin  45107  iinssf  45116  iindif2f  45138  disjrnmpt2  45166  disjinfi  45170  supxrleubrnmptf  45431  limcperiod  45610  limsupequzmptf  45713  dvnprodlem1  45928  stoweidlem16  45998  stoweidlem27  46009  stoweidlem28  46010  stoweidlem29  46011  stoweidlem31  46013  stoweidlem34  46016  stoweidlem35  46017  stoweidlem57  46039  stoweidlem59  46041  stirlinglem5  46060  fourierdlem16  46105  fourierdlem21  46110  fourierdlem22  46111  fourierdlem31  46120  fourierdlem48  46136  fourierdlem51  46139  fourierdlem80  46168  fourierdlem93  46181  etransclem32  46248  smfsupmpt  46797  smfinfmpt  46801  fsupdm  46824  cbvmpox2  48321  iinfssc  49043  iinfsubc  49044