Theorem nfcri 2914

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

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

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 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  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  5366  nfxp  5688  opeliunxp  5722  opeliun2xp  5723  iunxpf  5828  elrnmpt1  5944  nfmpo  7495  cbvmpox  7506  tfis  7851  fmpox  8064  nfsum1  15777  nfsum  15778  fsum2dlem  15856  fsumcom2  15860  nfcprod  15998  cbvprod  16002  fprod2dlem  16067  fprodcom2  16071  gsum2d2lem  20100  dprd2d2  20173  ptbasfi  23807  restmetu  24796  ovoliunnul  25735  iundisj  25776  iunmbl2  25785  nfitg  26002  limciun  26121  reuxfrdf  32966  abrexss  32987  cbviunf  33029  iunin1f  33031  cbvdisjf  33044  disjabrex  33055  disjabrexf  33056  iundisjf  33062  ssrelf  33088  2ndresdju  33122  fmptcof2  33130  acunirnmpt2f  33134  iundisjfi  33267  suppgsumssiun  33512  fedgmullem2  34140  irngnzply1  34201  locfinreflem  34350  esum2dlem  34602  oms0  34808  bnj1385  35341  bnj900  35438  bnj1014  35470  bnj1123  35495  bnj1228  35520  bnj1321  35536  bnj1384  35541  bnj1398  35543  bnj1408  35545  bnj1444  35552  bnj1445  35553  bnj1446  35554  bnj1449  35557  bnj1467  35563  bnj1518  35573  bj-nfcf  37666  mptsnunlem  38092  phpreu  38358  poimirlem26  38395  mbfposadd  38416  mpobi123f  38910  rababg  44414  ss2iundf  44499  binomcxplemnotnn0  45180  refsumcn  45864  cbvmpo2  45929  cbvmpo1  45930  iinssiin  45961  iinssf  45970  iindif2f  45992  disjrnmpt2  46020  disjinfi  46024  supxrleubrnmptf  46279  limcperiod  46458  limsupequzmptf  46559  dvnprodlem1  46774  stoweidlem16  46844  stoweidlem27  46855  stoweidlem28  46856  stoweidlem29  46857  stoweidlem31  46859  stoweidlem34  46862  stoweidlem35  46863  stoweidlem57  46885  stoweidlem59  46887  stirlinglem5  46906  fourierdlem16  46951  fourierdlem21  46956  fourierdlem22  46957  fourierdlem31  46966  fourierdlem48  46982  fourierdlem51  46985  fourierdlem80  47014  fourierdlem93  47027  etransclem32  47094  smfsupmpt  47643  smfinfmpt  47647  fsupdm  47670  cbvmpox2  49266  iinfssc  49983  iinfsubc  49984