Theorem nfcri 2917

Description: Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.) Avoid ax-10 2176, ax-11 2192. (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 2915	. 2 ⊢ (Ⅎ𝑥𝐴 → Ⅎ𝑥 𝑦 ∈ 𝐴)
3	1, 2	ax-mp 5	1 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴

Syntax hints:  Ⅎwnf 1813   ∈ wcel 2143  Ⅎwnfc 2910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-nf 1814  df-clel 2838  df-nfc 2912

This theorem is referenced by:  nfcrii  2920  clelsb1fw  2929  clelsb1f  2930  cleqf  2953  sbabel  2957  r2alf  3286  cbvralfw  3305  cbvralf  3349  nfrmow  3398  nfreuw  3399  cbvrabw  3451  nfrabw  3452  nfrab  3453  cbvrab  3454  rmo3f  3698  nfccdeq  3742  sbcabel  3832  cbvcsbw  3864  cbvcsb  3865  csbgfi  3874  cbvrabcsfw  3895  cbvralcsf  3896  cbvreucsf  3898  cbvrabcsf  3899  dfssf  3929  nfdif  4085  nfun  4125  nfin  4178  nfiun  4989  nfiin  4990  nfiung  4991  nfiing  4992  cbviun  5000  cbviin  5001  cbviung  5002  cbviing  5003  iunssf  5008  iunssfOLD  5009  iunxsngf  5059  cbvdisj  5087  nfdisjw  5089  nfdisj  5090  nfmpt  5210  cbvmptf  5212  cbvmptfg  5213  reusv2lem4  5374  nfxp  5696  opeliunxp  5730  opeliun2xp  5731  iunxpf  5836  elrnmpt1  5952  nfmpo  7494  cbvmpox  7505  tfis  7852  fmpox  8065  nfsum1  15743  nfsum  15744  fsum2dlem  15823  fsumcom2  15827  nfcprod  15965  cbvprod  15969  fprod2dlem  16036  fprodcom2  16040  gsum2d2lem  20044  dprd2d2  20117  ptbasfi  23719  restmetu  24708  ovoliunnul  25647  iundisj  25688  iunmbl2  25697  nfitg  25915  limciun  26034  reuxfrdf  32818  abrexss  32839  cbviunf  32881  iunin1f  32883  cbvdisjf  32897  disjabrex  32908  disjabrexf  32909  iundisjf  32915  ssrelf  32941  2ndresdju  32975  fmptcof2  32983  acunirnmpt2f  32987  iundisjfi  33122  suppgsumssiun  33373  fedgmullem2  34001  irngnzply1  34062  locfinreflem  34211  esum2dlem  34463  oms0  34668  bnj1385  35201  bnj900  35298  bnj1014  35330  bnj1123  35355  bnj1228  35380  bnj1321  35396  bnj1384  35401  bnj1398  35403  bnj1408  35405  bnj1444  35412  bnj1445  35413  bnj1446  35414  bnj1449  35417  bnj1467  35423  bnj1518  35433  bj-nfcf  37539  mptsnunlem  37965  phpreu  38236  poimirlem26  38278  mbfposadd  38299  mpobi123f  38792  rababg  44283  ss2iundf  44368  binomcxplemnotnn0  45049  refsumcn  45733  cbvmpo2  45798  cbvmpo1  45799  iinssiin  45830  iinssf  45839  iindif2f  45861  disjrnmpt2  45889  disjinfi  45893  supxrleubrnmptf  46148  limcperiod  46327  limsupequzmptf  46428  dvnprodlem1  46643  stoweidlem16  46713  stoweidlem27  46724  stoweidlem28  46725  stoweidlem29  46726  stoweidlem31  46728  stoweidlem34  46731  stoweidlem35  46732  stoweidlem57  46754  stoweidlem59  46756  stirlinglem5  46775  fourierdlem16  46820  fourierdlem21  46825  fourierdlem22  46826  fourierdlem31  46835  fourierdlem48  46851  fourierdlem51  46854  fourierdlem80  46883  fourierdlem93  46896  etransclem32  46963  smfsupmpt  47512  smfinfmpt  47516  fsupdm  47539  cbvmpox2  49099  iinfssc  49818  iinfsubc  49819