Theorem nfcri 2915

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

Syntax hints:  Ⅎwnf 1802   ∈ wcel 2141  Ⅎwnfc 2908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-nf 1803  df-clel 2836  df-nfc 2910

This theorem is referenced by:  nfcrii  2918  clelsb1fw  2927  clelsb1f  2928  cleqf  2951  sbabel  2955  r2alf  3282  cbvralfw  3301  cbvralf  3346  nfrmow  3395  nfreuw  3396  cbvrabw  3448  cbvrabwOLD  3449  nfrabw  3450  nfrab  3451  cbvrab  3452  rmo3f  3696  nfccdeq  3740  sbcabel  3831  cbvcsbw  3862  cbvcsb  3863  csbgfi  3872  cbvrabcsfw  3893  cbvralcsf  3894  cbvreucsf  3896  cbvrabcsf  3897  dfssf  3927  nfdif  4083  nfun  4123  nfin  4176  nfiun  4980  nfiin  4981  nfiung  4982  nfiing  4983  cbviun  4991  cbviin  4992  cbviung  4993  cbviing  4994  iunssf  4999  iunssfOLD  5000  iunxsngf  5048  cbvdisj  5076  nfdisjw  5078  nfdisj  5079  nfmpt  5197  cbvmptf  5199  cbvmptfg  5200  reusv2lem4  5357  nfxp  5678  opeliunxp  5712  opeliun2xp  5713  iunxpf  5818  elrnmpt1  5934  nfmpo  7474  cbvmpox  7485  tfis  7831  fmpox  8044  nfsum1  15700  nfsum  15701  fsum2dlem  15780  fsumcom2  15784  nfcprod  15922  cbvprod  15926  fprod2dlem  15993  fprodcom2  15997  gsum2d2lem  19996  dprd2d2  20069  ptbasfi  23621  restmetu  24610  ovoliunnul  25549  iundisj  25590  iunmbl2  25599  nfitg  25817  limciun  25936  reuxfrdf  32638  abrexss  32660  cbviunf  32704  iunin1f  32706  cbvdisjf  32720  disjabrex  32731  disjabrexf  32732  iundisjf  32738  ssrelf  32767  2ndresdju  32801  fmptcof2  32809  acunirnmpt2f  32813  iundisjfi  32948  suppgsumssiun  33213  fedgmullem2  33888  irngnzply1  33949  locfinreflem  34098  esum2dlem  34350  oms0  34555  bnj1385  35091  bnj900  35188  bnj1014  35220  bnj1123  35245  bnj1228  35270  bnj1321  35286  bnj1384  35291  bnj1398  35293  bnj1408  35295  bnj1444  35302  bnj1445  35303  bnj1446  35304  bnj1449  35307  bnj1467  35313  bnj1518  35323  bj-nfcf  37372  mptsnunlem  37796  phpreu  38067  poimirlem26  38109  mbfposadd  38130  mpobi123f  38625  rababg  44114  ss2iundf  44199  binomcxplemnotnn0  44896  refsumcn  45574  cbvmpo2  45639  cbvmpo1  45640  iinssiin  45671  iinssf  45680  iindif2f  45702  disjrnmpt2  45730  disjinfi  45734  supxrleubrnmptf  45989  limcperiod  46168  limsupequzmptf  46269  dvnprodlem1  46484  stoweidlem16  46554  stoweidlem27  46565  stoweidlem28  46566  stoweidlem29  46567  stoweidlem31  46569  stoweidlem34  46572  stoweidlem35  46573  stoweidlem57  46595  stoweidlem59  46597  stirlinglem5  46616  fourierdlem16  46661  fourierdlem21  46666  fourierdlem22  46667  fourierdlem31  46676  fourierdlem48  46692  fourierdlem51  46695  fourierdlem80  46724  fourierdlem93  46737  etransclem32  46804  smfsupmpt  47353  smfinfmpt  47357  fsupdm  47380  cbvmpox2  48922  iinfssc  49642  iinfsubc  49643