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  3258  cbvralfw  3278  nfralw  3285  cbvralf  3334  nfrmow  3385  nfreuw  3386  cbvrabw  3441  cbvrabwOLD  3442  nfrabw  3443  nfrab  3445  cbvrab  3446  rmo3f  3705  nfccdeq  3749  sbcabel  3841  cbvcsbw  3872  cbvcsb  3873  csbgfi  3882  cbvrabcsfw  3903  cbvralcsf  3904  cbvreucsf  3906  cbvrabcsf  3907  dfssf  3937  nfdif  4092  nfdifOLD  4093  nfun  4133  nfunOLD  4134  nfin  4187  nfinOLD  4188  nfiun  4987  nfiin  4988  nfiung  4989  nfiing  4990  cbviun  5000  cbviin  5001  cbviung  5002  cbviing  5003  iunssf  5008  iunxsngf  5056  cbvdisj  5084  nfdisjw  5086  nfdisj  5087  nfmpt  5205  cbvmptf  5207  cbvmptfg  5208  reusv2lem4  5356  nfxp  5671  opeliunxp  5705  opeliun2xp  5706  iunxpf  5812  elrnmpt1  5924  nfmpo  7471  cbvmpox  7482  tfis  7831  fmpox  8046  nfsum1  15656  nfsum  15657  fsum2dlem  15736  fsumcom2  15740  nfcprod  15875  cbvprod  15879  fprod2dlem  15946  fprodcom2  15950  gsum2d2lem  19903  dprd2d2  19976  ptbasfi  23468  restmetu  24458  ovoliunnul  25408  iundisj  25449  iunmbl2  25458  nfitg  25676  limciun  25795  reuxfrdf  32420  abrexss  32441  cbviunf  32484  iunin1f  32486  cbvdisjf  32500  disjabrex  32511  disjabrexf  32512  iundisjf  32518  ssrelf  32543  2ndresdju  32573  fmptcof2  32581  acunirnmpt2f  32585  iundisjfi  32719  fedgmullem2  33626  irngnzply1  33686  locfinreflem  33830  esum2dlem  34082  oms0  34288  bnj1385  34822  bnj900  34919  bnj1014  34951  bnj1123  34976  bnj1228  35001  bnj1321  35017  bnj1384  35022  bnj1398  35024  bnj1408  35026  bnj1444  35033  bnj1445  35034  bnj1446  35035  bnj1449  35038  bnj1467  35044  bnj1518  35054  bj-nfcf  36911  mptsnunlem  37326  phpreu  37598  poimirlem26  37640  mbfposadd  37661  mpobi123f  38156  rababg  43563  ss2iundf  43648  binomcxplemnotnn0  44345  refsumcn  45024  cbvmpo2  45091  cbvmpo1  45092  iinssiin  45123  iinssf  45132  iindif2f  45154  disjrnmpt2  45182  disjinfi  45186  supxrleubrnmptf  45447  limcperiod  45626  limsupequzmptf  45729  dvnprodlem1  45944  stoweidlem16  46014  stoweidlem27  46025  stoweidlem28  46026  stoweidlem29  46027  stoweidlem31  46029  stoweidlem34  46032  stoweidlem35  46033  stoweidlem57  46055  stoweidlem59  46057  stirlinglem5  46076  fourierdlem16  46121  fourierdlem21  46126  fourierdlem22  46127  fourierdlem31  46136  fourierdlem48  46152  fourierdlem51  46155  fourierdlem80  46184  fourierdlem93  46197  etransclem32  46264  smfsupmpt  46813  smfinfmpt  46817  fsupdm  46840  cbvmpox2  48324  iinfssc  49046  iinfsubc  49047