Theorem nfcri 2890

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

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

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

This theorem is referenced by:  nfcrii  2893  clelsb1fw  2902  clelsb1f  2903  cleqf  2927  sbabel  2931  r2alf  3263  cbvralfw  3284  nfralw  3291  cbvralf  3339  nfrmow  3392  nfreuw  3393  cbvrabw  3452  cbvrabwOLD  3453  nfrabw  3454  nfrabwOLD  3455  nfrab  3457  cbvrab  3458  rmo3f  3717  nfccdeq  3761  sbcabel  3853  cbvcsbw  3884  cbvcsb  3885  csbgfi  3894  cbvrabcsfw  3915  cbvralcsf  3916  cbvreucsf  3918  cbvrabcsf  3919  dfssf  3949  nfdif  4104  nfdifOLD  4105  nfun  4145  nfunOLD  4146  nfin  4199  nfinOLD  4200  nfiun  4999  nfiin  5000  nfiung  5001  nfiing  5002  cbviun  5012  cbviin  5013  cbviung  5014  cbviing  5015  iunssf  5020  iunxsngf  5068  cbvdisj  5096  nfdisjw  5098  nfdisj  5099  nfmpt  5219  cbvmptf  5221  cbvmptfg  5222  reusv2lem4  5371  nfxp  5687  opeliunxp  5721  opeliun2xp  5722  iunxpf  5828  elrnmpt1  5940  nfmpo  7489  cbvmpox  7500  tfis  7850  fmpox  8066  nfsum1  15706  nfsum  15707  fsum2dlem  15786  fsumcom2  15790  nfcprod  15925  cbvprod  15929  fprod2dlem  15996  fprodcom2  16000  gsum2d2lem  19954  dprd2d2  20027  ptbasfi  23519  restmetu  24509  ovoliunnul  25460  iundisj  25501  iunmbl2  25510  nfitg  25728  limciun  25847  reuxfrdf  32472  abrexss  32493  cbviunf  32536  iunin1f  32538  cbvdisjf  32552  disjabrex  32563  disjabrexf  32564  iundisjf  32570  ssrelf  32595  2ndresdju  32627  fmptcof2  32635  acunirnmpt2f  32639  iundisjfi  32773  fedgmullem2  33670  irngnzply1  33732  locfinreflem  33871  esum2dlem  34123  oms0  34329  bnj1385  34863  bnj900  34960  bnj1014  34992  bnj1123  35017  bnj1228  35042  bnj1321  35058  bnj1384  35063  bnj1398  35065  bnj1408  35067  bnj1444  35074  bnj1445  35075  bnj1446  35076  bnj1449  35079  bnj1467  35085  bnj1518  35095  bj-nfcf  36941  mptsnunlem  37356  phpreu  37628  poimirlem26  37670  mbfposadd  37691  mpobi123f  38186  rababg  43598  ss2iundf  43683  binomcxplemnotnn0  44380  refsumcn  45054  cbvmpo2  45121  cbvmpo1  45122  iinssiin  45153  iinssf  45162  iindif2f  45184  disjrnmpt2  45212  disjinfi  45216  supxrleubrnmptf  45478  limcperiod  45657  limsupequzmptf  45760  dvnprodlem1  45975  stoweidlem16  46045  stoweidlem27  46056  stoweidlem28  46057  stoweidlem29  46058  stoweidlem31  46060  stoweidlem34  46063  stoweidlem35  46064  stoweidlem57  46086  stoweidlem59  46088  stirlinglem5  46107  fourierdlem16  46152  fourierdlem21  46157  fourierdlem22  46158  fourierdlem31  46167  fourierdlem48  46183  fourierdlem51  46186  fourierdlem80  46215  fourierdlem93  46228  etransclem32  46295  smfsupmpt  46844  smfinfmpt  46848  fsupdm  46871  cbvmpox2  48311  iinfssc  49024  iinfsubc  49025