Theorem nfcri 2919

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

Syntax hints:  Ⅎwnf 1806   ∈ wcel 2145  Ⅎwnfc 2912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-nf 1807  df-clel 2840  df-nfc 2914

This theorem is referenced by:  nfcrii  2922  clelsb1fw  2931  clelsb1f  2932  cleqf  2955  sbabel  2959  r2alf  3286  cbvralfw  3305  cbvralf  3350  nfrmow  3399  nfreuw  3400  cbvrabw  3452  cbvrabwOLD  3453  nfrabw  3454  nfrab  3455  cbvrab  3456  rmo3f  3700  nfccdeq  3744  sbcabel  3834  cbvcsbw  3865  cbvcsb  3866  csbgfi  3875  cbvrabcsfw  3896  cbvralcsf  3897  cbvreucsf  3899  cbvrabcsf  3900  dfssf  3930  nfdif  4086  nfun  4126  nfin  4179  nfiun  4984  nfiin  4985  nfiung  4986  nfiing  4987  cbviun  4995  cbviin  4996  cbviung  4997  cbviing  4998  iunssf  5003  iunssfOLD  5004  iunxsngf  5054  cbvdisj  5082  nfdisjw  5084  nfdisj  5085  nfmpt  5203  cbvmptf  5205  cbvmptfg  5206  reusv2lem4  5363  nfxp  5685  opeliunxp  5719  opeliun2xp  5720  iunxpf  5825  elrnmpt1  5941  nfmpo  7482  cbvmpox  7493  tfis  7839  fmpox  8052  nfsum1  15731  nfsum  15732  fsum2dlem  15811  fsumcom2  15815  nfcprod  15953  cbvprod  15957  fprod2dlem  16024  fprodcom2  16028  gsum2d2lem  20034  dprd2d2  20107  ptbasfi  23699  restmetu  24688  ovoliunnul  25627  iundisj  25668  iunmbl2  25677  nfitg  25895  limciun  26014  reuxfrdf  32747  abrexss  32768  cbviunf  32810  iunin1f  32812  cbvdisjf  32826  disjabrex  32837  disjabrexf  32838  iundisjf  32844  ssrelf  32872  2ndresdju  32906  fmptcof2  32914  acunirnmpt2f  32918  iundisjfi  33053  suppgsumssiun  33305  fedgmullem2  33937  irngnzply1  33998  locfinreflem  34147  esum2dlem  34399  oms0  34604  bnj1385  35137  bnj900  35234  bnj1014  35266  bnj1123  35291  bnj1228  35316  bnj1321  35332  bnj1384  35337  bnj1398  35339  bnj1408  35341  bnj1444  35348  bnj1445  35349  bnj1446  35350  bnj1449  35353  bnj1467  35359  bnj1518  35369  bj-nfcf  37420  mptsnunlem  37844  phpreu  38115  poimirlem26  38157  mbfposadd  38178  mpobi123f  38673  rababg  44162  ss2iundf  44247  binomcxplemnotnn0  44930  refsumcn  45608  cbvmpo2  45673  cbvmpo1  45674  iinssiin  45705  iinssf  45714  iindif2f  45736  disjrnmpt2  45764  disjinfi  45768  supxrleubrnmptf  46023  limcperiod  46202  limsupequzmptf  46303  dvnprodlem1  46518  stoweidlem16  46588  stoweidlem27  46599  stoweidlem28  46600  stoweidlem29  46601  stoweidlem31  46603  stoweidlem34  46606  stoweidlem35  46607  stoweidlem57  46629  stoweidlem59  46631  stirlinglem5  46650  fourierdlem16  46695  fourierdlem21  46700  fourierdlem22  46701  fourierdlem31  46710  fourierdlem48  46726  fourierdlem51  46729  fourierdlem80  46758  fourierdlem93  46771  etransclem32  46838  smfsupmpt  47387  smfinfmpt  47391  fsupdm  47414  cbvmpox2  48967  iinfssc  49686  iinfsubc  49687