Theorem nfcri 2914

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

This proof depends on syntax axioms:  Ⅎwnf 1815   ∈ wcel 2144  Ⅎwnfc 2907

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-nf 1816  df-clel 2835  df-nfc 2909

This theorem is used by:  nfcrii  2917  clelsb1fw  2926  clelsb1f  2927  cleqf  2950  sbabel  2954  r2alf  3283  cbvralfw  3302  cbvralf  3345  nfrmow  3394  nfreuw  3395  cbvrabw  3446  nfrabw  3447  nfrab  3448  cbvrab  3449  rmo3f  3691  nfccdeq  3735  sbcabel  3824  cbvcsbw  3856  cbvcsb  3857  csbgfi  3866  cbvrabcsfw  3887  cbvralcsf  3888  cbvreucsf  3890  cbvrabcsf  3891  dfssf  3899  nfdif  4066  nfin  4121  nfun  4169  nfiun  4981  nfiin  4982  nfiung  4983  nfiing  4984  cbviun  4992  cbviin  4993  cbviung  4994  cbviing  4995  iunssf  5000  iunssfOLD  5001  iunxsngf  5051  cbvdisj  5079  nfdisjw  5081  nfdisj  5082  nfmpt  5202  cbvmptf  5204  cbvmptfg  5205  reusv2lem4  5362  nfxp  5683  opeliunxp  5717  opeliun2xp  5718  iunxpf  5825  elrnmpt1  5941  nfmpo  7502  cbvmpox  7513  tfis  7866  fmpox  8078  nfsum1  15857  nfsum  15858  fsum2dlem  15936  fsumcom2  15940  nfcprod  16078  cbvprod  16082  fprod2dlem  16147  fprodcom2  16151  gsum2d2lem  20187  dprd2d2  20260  ptbasfi  23900  restmetu  24889  ovoliunnul  25828  iundisj  25869  iunmbl2  25878  nfitg  26095  limciun  26214  reuxfrdf  33129  abrexss  33150  cbviunf  33192  iunin1f  33194  cbvdisjf  33207  disjabrex  33218  disjabrexf  33219  iundisjf  33225  ssrelf  33251  2ndresdju  33285  fmptcof2  33293  acunirnmpt2f  33297  iundisjfi  33430  suppgsumssiun  33675  fedgmullem2  34304  irngnzply1  34365  locfinreflem  34514  esum2dlem  34766  oms0  34971  bnj1385  35504  bnj900  35601  bnj1014  35633  bnj1123  35658  bnj1228  35683  bnj1321  35699  bnj1384  35704  bnj1398  35706  bnj1408  35708  bnj1444  35715  bnj1445  35716  bnj1446  35717  bnj1449  35720  bnj1467  35726  bnj1518  35736  bj-nfcf  37877  mptsnunlem  38304  phpreu  38570  poimirlem26  38607  mbfposadd  38628  mpobi123f  39137  rababg  44617  ss2iundf  44701  binomcxplemnotnn0  45382  refsumcn  46089  cbvmpo2  46154  cbvmpo1  46155  iinssiin  46186  iinssf  46195  iindif2f  46217  disjrnmpt2  46245  disjinfi  46249  supxrleubrnmptf  46503  limcperiod  46682  limsupequzmptf  46783  dvnprodlem1  46998  stoweidlem16  47068  stoweidlem27  47079  stoweidlem28  47080  stoweidlem29  47081  stoweidlem31  47083  stoweidlem34  47086  stoweidlem35  47087  stoweidlem57  47109  stoweidlem59  47111  stirlinglem5  47130  fourierdlem16  47175  fourierdlem21  47180  fourierdlem22  47181  fourierdlem31  47190  fourierdlem48  47206  fourierdlem51  47209  fourierdlem80  47238  fourierdlem93  47251  etransclem32  47318  smfsupmpt  47867  smfinfmpt  47871  fsupdm  47894  cbvmpox2  49490  iinfssc  50207  iinfsubc  50208