Theorem nfcri 2894

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

Syntax hints:  Ⅎwnf 1790   ∈ wcel 2119  Ⅎwnfc 2887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-nf 1791  df-clel 2815  df-nfc 2889

This theorem is referenced by:  nfcrii  2897  clelsb1fw  2906  clelsb1f  2907  cleqf  2930  sbabel  2934  r2alf  3261  cbvralfw  3280  cbvralf  3325  nfrmow  3374  nfreuw  3375  cbvrabw  3427  cbvrabwOLD  3428  nfrabw  3429  nfrab  3430  cbvrab  3431  rmo3f  3682  nfccdeq  3726  sbcabel  3817  cbvcsbw  3848  cbvcsb  3849  csbgfi  3858  cbvrabcsfw  3879  cbvralcsf  3880  cbvreucsf  3882  cbvrabcsf  3883  dfssf  3913  nfdif  4067  nfun  4107  nfin  4160  nfiun  4960  nfiin  4961  nfiung  4962  nfiing  4963  cbviun  4971  cbviin  4972  cbviung  4973  cbviing  4974  iunssf  4979  iunssfOLD  4980  iunxsngf  5028  cbvdisj  5056  nfdisjw  5058  nfdisj  5059  nfmpt  5177  cbvmptf  5179  cbvmptfg  5180  reusv2lem4  5337  nfxp  5658  opeliunxp  5692  opeliun2xp  5693  iunxpf  5797  elrnmpt1  5909  nfmpo  7445  cbvmpox  7456  tfis  7802  fmpox  8016  nfsum1  15650  nfsum  15651  fsum2dlem  15730  fsumcom2  15734  nfcprod  15872  cbvprod  15876  fprod2dlem  15943  fprodcom2  15947  gsum2d2lem  19946  dprd2d2  20019  ptbasfi  23571  restmetu  24560  ovoliunnul  25499  iundisj  25540  iunmbl2  25549  nfitg  25767  limciun  25886  reuxfrdf  32585  abrexss  32607  cbviunf  32651  iunin1f  32653  cbvdisjf  32667  disjabrex  32678  disjabrexf  32679  iundisjf  32685  ssrelf  32714  2ndresdju  32748  fmptcof2  32756  acunirnmpt2f  32760  iundisjfi  32895  suppgsumssiun  33160  fedgmullem2  33821  irngnzply1  33882  locfinreflem  34031  esum2dlem  34283  oms0  34488  bnj1385  35021  bnj900  35118  bnj1014  35150  bnj1123  35175  bnj1228  35200  bnj1321  35216  bnj1384  35221  bnj1398  35223  bnj1408  35225  bnj1444  35232  bnj1445  35233  bnj1446  35234  bnj1449  35237  bnj1467  35243  bnj1518  35253  bj-nfcf  37283  mptsnunlem  37707  phpreu  37978  poimirlem26  38020  mbfposadd  38041  mpobi123f  38536  rababg  44025  ss2iundf  44110  binomcxplemnotnn0  44807  refsumcn  45485  cbvmpo2  45551  cbvmpo1  45552  iinssiin  45583  iinssf  45592  iindif2f  45614  disjrnmpt2  45642  disjinfi  45646  supxrleubrnmptf  45901  limcperiod  46080  limsupequzmptf  46181  dvnprodlem1  46396  stoweidlem16  46466  stoweidlem27  46477  stoweidlem28  46478  stoweidlem29  46479  stoweidlem31  46481  stoweidlem34  46484  stoweidlem35  46485  stoweidlem57  46507  stoweidlem59  46509  stirlinglem5  46528  fourierdlem16  46573  fourierdlem21  46578  fourierdlem22  46579  fourierdlem31  46588  fourierdlem48  46604  fourierdlem51  46607  fourierdlem80  46636  fourierdlem93  46649  etransclem32  46716  smfsupmpt  47265  smfinfmpt  47269  fsupdm  47292  cbvmpox2  48834  iinfssc  49554  iinfsubc  49555