Theorem nfcri 2884

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 2882	. 2 ⊢ (Ⅎ𝑥𝐴 → Ⅎ𝑥 𝑦 ∈ 𝐴)
3	1, 2	ax-mp 5	1 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴

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

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 2804  df-nfc 2879

This theorem is referenced by:  nfcrii  2887  clelsb1fw  2896  clelsb1f  2897  cleqf  2921  sbabel  2925  r2alf  3259  cbvralfw  3280  nfralw  3287  cbvralf  3336  nfrmow  3387  nfreuw  3388  cbvrabw  3444  cbvrabwOLD  3445  nfrabw  3446  nfrab  3448  cbvrab  3449  rmo3f  3708  nfccdeq  3752  sbcabel  3844  cbvcsbw  3875  cbvcsb  3876  csbgfi  3885  cbvrabcsfw  3906  cbvralcsf  3907  cbvreucsf  3909  cbvrabcsf  3910  dfssf  3940  nfdif  4095  nfdifOLD  4096  nfun  4136  nfunOLD  4137  nfin  4190  nfinOLD  4191  nfiun  4990  nfiin  4991  nfiung  4992  nfiing  4993  cbviun  5003  cbviin  5004  cbviung  5005  cbviing  5006  iunssf  5011  iunxsngf  5059  cbvdisj  5087  nfdisjw  5089  nfdisj  5090  nfmpt  5208  cbvmptf  5210  cbvmptfg  5211  reusv2lem4  5359  nfxp  5674  opeliunxp  5708  opeliun2xp  5709  iunxpf  5815  elrnmpt1  5927  nfmpo  7474  cbvmpox  7485  tfis  7834  fmpox  8049  nfsum1  15663  nfsum  15664  fsum2dlem  15743  fsumcom2  15747  nfcprod  15882  cbvprod  15886  fprod2dlem  15953  fprodcom2  15957  gsum2d2lem  19910  dprd2d2  19983  ptbasfi  23475  restmetu  24465  ovoliunnul  25415  iundisj  25456  iunmbl2  25465  nfitg  25683  limciun  25802  reuxfrdf  32427  abrexss  32448  cbviunf  32491  iunin1f  32493  cbvdisjf  32507  disjabrex  32518  disjabrexf  32519  iundisjf  32525  ssrelf  32550  2ndresdju  32580  fmptcof2  32588  acunirnmpt2f  32592  iundisjfi  32726  fedgmullem2  33633  irngnzply1  33693  locfinreflem  33837  esum2dlem  34089  oms0  34295  bnj1385  34829  bnj900  34926  bnj1014  34958  bnj1123  34983  bnj1228  35008  bnj1321  35024  bnj1384  35029  bnj1398  35031  bnj1408  35033  bnj1444  35040  bnj1445  35041  bnj1446  35042  bnj1449  35045  bnj1467  35051  bnj1518  35061  bj-nfcf  36918  mptsnunlem  37333  phpreu  37605  poimirlem26  37647  mbfposadd  37668  mpobi123f  38163  rababg  43570  ss2iundf  43655  binomcxplemnotnn0  44352  refsumcn  45031  cbvmpo2  45098  cbvmpo1  45099  iinssiin  45130  iinssf  45139  iindif2f  45161  disjrnmpt2  45189  disjinfi  45193  supxrleubrnmptf  45454  limcperiod  45633  limsupequzmptf  45736  dvnprodlem1  45951  stoweidlem16  46021  stoweidlem27  46032  stoweidlem28  46033  stoweidlem29  46034  stoweidlem31  46036  stoweidlem34  46039  stoweidlem35  46040  stoweidlem57  46062  stoweidlem59  46064  stirlinglem5  46083  fourierdlem16  46128  fourierdlem21  46133  fourierdlem22  46134  fourierdlem31  46143  fourierdlem48  46159  fourierdlem51  46162  fourierdlem80  46191  fourierdlem93  46204  etransclem32  46271  smfsupmpt  46820  smfinfmpt  46824  fsupdm  46847  cbvmpox2  48328  iinfssc  49050  iinfsubc  49051