Theorem nfcri 2915

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

This proof depends on syntax axioms:  Ⅎwnf 1816   ∈ wcel 2145  Ⅎwnfc 2908

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-nf 1817  df-clel 2836  df-nfc 2910

This theorem is used by:  nfcrii  2918  clelsb1fw  2927  clelsb1f  2928  cleqf  2951  sbabel  2955  r2alf  3284  cbvralfw  3303  cbvralf  3346  nfrmow  3395  nfreuw  3396  cbvrabw  3447  nfrabw  3448  nfrab  3449  cbvrab  3450  rmo3f  3692  nfccdeq  3736  sbcabel  3825  cbvcsbw  3857  cbvcsb  3858  csbgfi  3867  cbvrabcsfw  3888  cbvralcsf  3889  cbvreucsf  3891  cbvrabcsf  3892  dfssf  3922  nfdif  4077  nfun  4117  nfin  4170  nfiun  4982  nfiin  4983  nfiung  4984  nfiing  4985  cbviun  4993  cbviin  4994  cbviung  4995  cbviing  4996  iunssf  5001  iunssfOLD  5002  iunxsngf  5052  cbvdisj  5080  nfdisjw  5082  nfdisj  5083  nfmpt  5203  cbvmptf  5205  cbvmptfg  5206  reusv2lem4  5363  nfxp  5684  opeliunxp  5718  opeliun2xp  5719  iunxpf  5826  elrnmpt1  5942  nfmpo  7500  cbvmpox  7511  tfis  7864  fmpox  8076  nfsum1  15850  nfsum  15851  fsum2dlem  15929  fsumcom2  15933  nfcprod  16071  cbvprod  16075  fprod2dlem  16140  fprodcom2  16144  gsum2d2lem  20180  dprd2d2  20253  ptbasfi  23893  restmetu  24882  ovoliunnul  25821  iundisj  25862  iunmbl2  25871  nfitg  26088  limciun  26207  reuxfrdf  33080  abrexss  33101  cbviunf  33143  iunin1f  33145  cbvdisjf  33158  disjabrex  33169  disjabrexf  33170  iundisjf  33176  ssrelf  33202  2ndresdju  33236  fmptcof2  33244  acunirnmpt2f  33248  iundisjfi  33381  suppgsumssiun  33626  fedgmullem2  34255  irngnzply1  34316  locfinreflem  34465  esum2dlem  34717  oms0  34922  bnj1385  35455  bnj900  35552  bnj1014  35584  bnj1123  35609  bnj1228  35634  bnj1321  35650  bnj1384  35655  bnj1398  35657  bnj1408  35659  bnj1444  35666  bnj1445  35667  bnj1446  35668  bnj1449  35671  bnj1467  35677  bnj1518  35687  bj-nfcf  37815  mptsnunlem  38241  phpreu  38507  poimirlem26  38544  mbfposadd  38565  mpobi123f  39074  rababg  44559  ss2iundf  44644  binomcxplemnotnn0  45325  refsumcn  46016  cbvmpo2  46081  cbvmpo1  46082  iinssiin  46113  iinssf  46122  iindif2f  46144  disjrnmpt2  46172  disjinfi  46176  supxrleubrnmptf  46430  limcperiod  46609  limsupequzmptf  46710  dvnprodlem1  46925  stoweidlem16  46995  stoweidlem27  47006  stoweidlem28  47007  stoweidlem29  47008  stoweidlem31  47010  stoweidlem34  47013  stoweidlem35  47014  stoweidlem57  47036  stoweidlem59  47038  stirlinglem5  47057  fourierdlem16  47102  fourierdlem21  47107  fourierdlem22  47108  fourierdlem31  47117  fourierdlem48  47133  fourierdlem51  47136  fourierdlem80  47165  fourierdlem93  47178  etransclem32  47245  smfsupmpt  47794  smfinfmpt  47798  fsupdm  47821  cbvmpox2  49417  iinfssc  50134  iinfsubc  50135