Theorem nfcri 2891

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

Syntax hints:  Ⅎwnf 1785   ∈ wcel 2114  Ⅎwnfc 2884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-nf 1786  df-clel 2812  df-nfc 2886

This theorem is referenced by:  nfcrii  2894  clelsb1fw  2903  clelsb1f  2904  cleqf  2928  sbabel  2932  r2alf  3259  cbvralfw  3278  nfralw  3285  cbvralf  3332  nfrmow  3381  nfreuw  3382  cbvrabw  3436  cbvrabwOLD  3437  nfrabw  3438  nfrab  3440  cbvrab  3441  rmo3f  3694  nfccdeq  3738  sbcabel  3830  cbvcsbw  3861  cbvcsb  3862  csbgfi  3871  cbvrabcsfw  3892  cbvralcsf  3893  cbvreucsf  3895  cbvrabcsf  3896  dfssf  3926  nfdif  4083  nfdifOLD  4084  nfun  4124  nfunOLD  4125  nfin  4178  nfinOLD  4179  nfiun  4980  nfiin  4981  nfiung  4982  nfiing  4983  cbviun  4992  cbviin  4993  cbviung  4994  cbviing  4995  iunssf  5000  iunssfOLD  5001  iunxsngf  5049  cbvdisj  5077  nfdisjw  5079  nfdisj  5080  nfmpt  5198  cbvmptf  5200  cbvmptfg  5201  reusv2lem4  5348  nfxp  5665  opeliunxp  5699  opeliun2xp  5700  iunxpf  5805  elrnmpt1  5917  nfmpo  7450  cbvmpox  7461  tfis  7807  fmpox  8021  nfsum1  15625  nfsum  15626  fsum2dlem  15705  fsumcom2  15709  nfcprod  15844  cbvprod  15848  fprod2dlem  15915  fprodcom2  15919  gsum2d2lem  19914  dprd2d2  19987  ptbasfi  23537  restmetu  24526  ovoliunnul  25476  iundisj  25517  iunmbl2  25526  nfitg  25744  limciun  25863  reuxfrdf  32576  abrexss  32598  cbviunf  32641  iunin1f  32643  cbvdisjf  32657  disjabrex  32668  disjabrexf  32669  iundisjf  32675  ssrelf  32704  2ndresdju  32738  fmptcof2  32746  acunirnmpt2f  32750  iundisjfi  32886  suppgsumssiun  33165  fedgmullem2  33807  irngnzply1  33868  locfinreflem  34017  esum2dlem  34269  oms0  34474  bnj1385  35007  bnj900  35104  bnj1014  35136  bnj1123  35161  bnj1228  35186  bnj1321  35202  bnj1384  35207  bnj1398  35209  bnj1408  35211  bnj1444  35218  bnj1445  35219  bnj1446  35220  bnj1449  35223  bnj1467  35229  bnj1518  35239  bj-nfcf  37165  mptsnunlem  37587  phpreu  37849  poimirlem26  37891  mbfposadd  37912  mpobi123f  38407  rababg  43924  ss2iundf  44009  binomcxplemnotnn0  44706  refsumcn  45384  cbvmpo2  45450  cbvmpo1  45451  iinssiin  45482  iinssf  45491  iindif2f  45513  disjrnmpt2  45541  disjinfi  45545  supxrleubrnmptf  45803  limcperiod  45982  limsupequzmptf  46083  dvnprodlem1  46298  stoweidlem16  46368  stoweidlem27  46379  stoweidlem28  46380  stoweidlem29  46381  stoweidlem31  46383  stoweidlem34  46386  stoweidlem35  46387  stoweidlem57  46409  stoweidlem59  46411  stirlinglem5  46430  fourierdlem16  46475  fourierdlem21  46480  fourierdlem22  46481  fourierdlem31  46490  fourierdlem48  46506  fourierdlem51  46509  fourierdlem80  46538  fourierdlem93  46551  etransclem32  46618  smfsupmpt  47167  smfinfmpt  47171  fsupdm  47194  cbvmpox2  48690  iinfssc  49410  iinfsubc  49411