Theorem nfcri 2887

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

Syntax hints:  Ⅎwnf 1784   ∈ wcel 2113  Ⅎwnfc 2880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-nf 1785  df-clel 2808  df-nfc 2882

This theorem is referenced by:  nfcrii  2890  clelsb1fw  2899  clelsb1f  2900  cleqf  2924  sbabel  2928  r2alf  3254  cbvralfw  3273  nfralw  3280  cbvralf  3327  nfrmow  3376  nfreuw  3377  cbvrabw  3431  cbvrabwOLD  3432  nfrabw  3433  nfrab  3435  cbvrab  3436  rmo3f  3689  nfccdeq  3733  sbcabel  3825  cbvcsbw  3856  cbvcsb  3857  csbgfi  3866  cbvrabcsfw  3887  cbvralcsf  3888  cbvreucsf  3890  cbvrabcsf  3891  dfssf  3921  nfdif  4078  nfdifOLD  4079  nfun  4119  nfunOLD  4120  nfin  4173  nfinOLD  4174  nfiun  4973  nfiin  4974  nfiung  4975  nfiing  4976  cbviun  4985  cbviin  4986  cbviung  4987  cbviing  4988  iunssf  4993  iunssfOLD  4994  iunxsngf  5042  cbvdisj  5070  nfdisjw  5072  nfdisj  5073  nfmpt  5191  cbvmptf  5193  cbvmptfg  5194  reusv2lem4  5341  nfxp  5652  opeliunxp  5686  opeliun2xp  5687  iunxpf  5792  elrnmpt1  5904  nfmpo  7434  cbvmpox  7445  tfis  7791  fmpox  8005  nfsum1  15599  nfsum  15600  fsum2dlem  15679  fsumcom2  15683  nfcprod  15818  cbvprod  15822  fprod2dlem  15889  fprodcom2  15893  gsum2d2lem  19887  dprd2d2  19960  ptbasfi  23497  restmetu  24486  ovoliunnul  25436  iundisj  25477  iunmbl2  25486  nfitg  25704  limciun  25823  reuxfrdf  32472  abrexss  32494  cbviunf  32537  iunin1f  32539  cbvdisjf  32553  disjabrex  32564  disjabrexf  32565  iundisjf  32571  ssrelf  32600  2ndresdju  32633  fmptcof2  32641  acunirnmpt2f  32645  iundisjfi  32783  fedgmullem2  33664  irngnzply1  33725  locfinreflem  33874  esum2dlem  34126  oms0  34331  bnj1385  34865  bnj900  34962  bnj1014  34994  bnj1123  35019  bnj1228  35044  bnj1321  35060  bnj1384  35065  bnj1398  35067  bnj1408  35069  bnj1444  35076  bnj1445  35077  bnj1446  35078  bnj1449  35081  bnj1467  35087  bnj1518  35097  bj-nfcf  36988  mptsnunlem  37403  phpreu  37664  poimirlem26  37706  mbfposadd  37727  mpobi123f  38222  rababg  43691  ss2iundf  43776  binomcxplemnotnn0  44473  refsumcn  45151  cbvmpo2  45218  cbvmpo1  45219  iinssiin  45250  iinssf  45259  iindif2f  45281  disjrnmpt2  45309  disjinfi  45313  supxrleubrnmptf  45573  limcperiod  45752  limsupequzmptf  45853  dvnprodlem1  46068  stoweidlem16  46138  stoweidlem27  46149  stoweidlem28  46150  stoweidlem29  46151  stoweidlem31  46153  stoweidlem34  46156  stoweidlem35  46157  stoweidlem57  46179  stoweidlem59  46181  stirlinglem5  46200  fourierdlem16  46245  fourierdlem21  46250  fourierdlem22  46251  fourierdlem31  46260  fourierdlem48  46276  fourierdlem51  46279  fourierdlem80  46308  fourierdlem93  46321  etransclem32  46388  smfsupmpt  46937  smfinfmpt  46941  fsupdm  46964  cbvmpox2  48460  iinfssc  49182  iinfsubc  49183