Theorem nfcri 2897

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

Syntax hints:  Ⅎwnf 1783   ∈ wcel 2108  Ⅎwnfc 2890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-nf 1784  df-clel 2816  df-nfc 2892

This theorem is referenced by:  nfcrii  2900  clelsb1fw  2909  clelsb1f  2910  cleqf  2934  sbabel  2938  sbabelOLD  2939  r2alf  3281  cbvralfw  3304  nfralw  3311  cbvralf  3360  nfrmow  3413  nfreuw  3414  cbvrabw  3473  cbvrabwOLD  3474  nfrabw  3475  nfrabwOLD  3476  nfrab  3478  cbvrab  3479  rmo3f  3740  nfccdeq  3784  sbcabel  3878  cbvcsbw  3909  cbvcsb  3910  csbgfi  3919  cbvrabcsfw  3940  cbvralcsf  3941  cbvreucsf  3943  cbvrabcsf  3944  dfssf  3974  nfdif  4129  nfdifOLD  4130  nfun  4170  nfunOLD  4171  nfin  4224  nfinOLD  4225  nfiun  5023  nfiin  5024  nfiung  5025  nfiing  5026  cbviun  5036  cbviin  5037  cbviung  5038  cbviing  5039  iunssf  5044  iunxsngf  5092  cbvdisj  5120  nfdisjw  5122  nfdisj  5123  nfmpt  5249  cbvmptf  5251  cbvmptfg  5252  reusv2lem4  5401  nfxp  5718  opeliunxp  5752  opeliun2xp  5753  iunxpf  5859  elrnmpt1  5971  nfmpo  7515  cbvmpox  7526  tfis  7876  fmpox  8092  nfsum1  15726  nfsum  15727  fsum2dlem  15806  fsumcom2  15810  nfcprod  15945  cbvprod  15949  fprod2dlem  16016  fprodcom2  16020  gsum2d2lem  19991  dprd2d2  20064  ptbasfi  23589  restmetu  24583  ovoliunnul  25542  iundisj  25583  iunmbl2  25592  nfitg  25810  limciun  25929  reuxfrdf  32510  abrexss  32531  cbviunf  32568  iunin1f  32570  cbvdisjf  32584  disjabrex  32595  disjabrexf  32596  iundisjf  32602  ssrelf  32627  2ndresdju  32659  fmptcof2  32667  acunirnmpt2f  32671  iundisjfi  32798  fedgmullem2  33681  irngnzply1  33741  locfinreflem  33839  esum2dlem  34093  oms0  34299  bnj1385  34846  bnj900  34943  bnj1014  34975  bnj1123  35000  bnj1228  35025  bnj1321  35041  bnj1384  35046  bnj1398  35048  bnj1408  35050  bnj1444  35057  bnj1445  35058  bnj1446  35059  bnj1449  35062  bnj1467  35068  bnj1518  35078  bj-nfcf  36924  mptsnunlem  37339  phpreu  37611  poimirlem26  37653  mbfposadd  37674  mpobi123f  38169  rababg  43587  ss2iundf  43672  binomcxplemnotnn0  44375  refsumcn  45035  cbvmpo2  45102  cbvmpo1  45103  iinssiin  45134  iinssf  45143  iindif2f  45165  disjrnmpt2  45193  disjinfi  45197  supxrleubrnmptf  45462  limcperiod  45643  limsupequzmptf  45746  dvnprodlem1  45961  stoweidlem16  46031  stoweidlem27  46042  stoweidlem28  46043  stoweidlem29  46044  stoweidlem31  46046  stoweidlem34  46049  stoweidlem35  46050  stoweidlem57  46072  stoweidlem59  46074  stirlinglem5  46093  fourierdlem16  46138  fourierdlem21  46143  fourierdlem22  46144  fourierdlem31  46153  fourierdlem48  46169  fourierdlem51  46172  fourierdlem80  46201  fourierdlem93  46214  etransclem32  46281  smfsupmpt  46830  smfinfmpt  46834  fsupdm  46857  cbvmpox2  48252