Theorem nfcri 2890

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

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

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 2811  df-nfc 2885

This theorem is referenced by:  nfcrii  2893  clelsb1fw  2902  clelsb1f  2903  cleqf  2927  sbabel  2931  r2alf  3258  cbvralfw  3277  cbvralf  3322  nfrmow  3371  nfreuw  3372  cbvrabw  3424  cbvrabwOLD  3425  nfrabw  3426  nfrab  3427  cbvrab  3428  rmo3f  3680  nfccdeq  3724  sbcabel  3816  cbvcsbw  3847  cbvcsb  3848  csbgfi  3857  cbvrabcsfw  3878  cbvralcsf  3879  cbvreucsf  3881  cbvrabcsf  3882  dfssf  3912  nfdif  4069  nfdifOLD  4070  nfun  4110  nfunOLD  4111  nfin  4164  nfinOLD  4165  nfiun  4965  nfiin  4966  nfiung  4967  nfiing  4968  cbviun  4977  cbviin  4978  cbviung  4979  cbviing  4980  iunssf  4985  iunssfOLD  4986  iunxsngf  5034  cbvdisj  5062  nfdisjw  5064  nfdisj  5065  nfmpt  5183  cbvmptf  5185  cbvmptfg  5186  reusv2lem4  5343  nfxp  5664  opeliunxp  5698  opeliun2xp  5699  iunxpf  5803  elrnmpt1  5915  nfmpo  7449  cbvmpox  7460  tfis  7806  fmpox  8020  nfsum1  15652  nfsum  15653  fsum2dlem  15732  fsumcom2  15736  nfcprod  15874  cbvprod  15878  fprod2dlem  15945  fprodcom2  15949  gsum2d2lem  19948  dprd2d2  20021  ptbasfi  23546  restmetu  24535  ovoliunnul  25474  iundisj  25515  iunmbl2  25524  nfitg  25742  limciun  25861  reuxfrdf  32560  abrexss  32582  cbviunf  32625  iunin1f  32627  cbvdisjf  32641  disjabrex  32652  disjabrexf  32653  iundisjf  32659  ssrelf  32688  2ndresdju  32722  fmptcof2  32730  acunirnmpt2f  32734  iundisjfi  32869  suppgsumssiun  33133  fedgmullem2  33774  irngnzply1  33835  locfinreflem  33984  esum2dlem  34236  oms0  34441  bnj1385  34974  bnj900  35071  bnj1014  35103  bnj1123  35128  bnj1228  35153  bnj1321  35169  bnj1384  35174  bnj1398  35176  bnj1408  35178  bnj1444  35185  bnj1445  35186  bnj1446  35187  bnj1449  35190  bnj1467  35196  bnj1518  35206  bj-nfcf  37230  mptsnunlem  37654  phpreu  37925  poimirlem26  37967  mbfposadd  37988  mpobi123f  38483  rababg  44001  ss2iundf  44086  binomcxplemnotnn0  44783  refsumcn  45461  cbvmpo2  45527  cbvmpo1  45528  iinssiin  45559  iinssf  45568  iindif2f  45590  disjrnmpt2  45618  disjinfi  45622  supxrleubrnmptf  45879  limcperiod  46058  limsupequzmptf  46159  dvnprodlem1  46374  stoweidlem16  46444  stoweidlem27  46455  stoweidlem28  46456  stoweidlem29  46457  stoweidlem31  46459  stoweidlem34  46462  stoweidlem35  46463  stoweidlem57  46485  stoweidlem59  46487  stirlinglem5  46506  fourierdlem16  46551  fourierdlem21  46556  fourierdlem22  46557  fourierdlem31  46566  fourierdlem48  46582  fourierdlem51  46585  fourierdlem80  46614  fourierdlem93  46627  etransclem32  46694  smfsupmpt  47243  smfinfmpt  47247  fsupdm  47270  cbvmpox2  48812  iinfssc  49532  iinfsubc  49533