Theorem nfcri 2882

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

Syntax hints:  Ⅎwnf 1777   ∈ wcel 2098  Ⅎwnfc 2875

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1774  df-nf 1778  df-clel 2802  df-nfc 2877

This theorem is referenced by:  nfcrii  2887  nfcriiOLD  2888  clelsb1fw  2899  clelsb1f  2900  cleqf  2926  sbabel  2930  sbabelOLD  2931  r2alf  3270  cbvralfw  3293  nfralw  3300  cbvralfwOLD  3312  cbvralf  3348  nfrmow  3401  nfreuw  3402  cbvrabw  3459  nfrabw  3460  nfrabwOLD  3461  nfrab  3464  cbvrab  3465  rmo3f  3722  nfccdeq  3766  sbcabel  3864  cbvcsbw  3895  cbvcsb  3896  csbgfi  3906  cbvrabcsfw  3929  cbvralcsf  3930  cbvreucsf  3932  cbvrabcsf  3933  dfss2f  3964  nfdif  4117  nfun  4157  nfin  4208  nfiun  5017  nfiin  5018  nfiung  5019  nfiing  5020  cbviun  5029  cbviin  5030  cbviung  5031  cbviing  5032  iunssf  5037  iunxsngf  5085  cbvdisj  5113  nfdisjw  5115  nfdisj  5116  nfmpt  5245  cbvmptf  5247  cbvmptfg  5248  reusv2lem4  5389  nfxp  5699  opeliunxp  5733  iunxpf  5838  elrnmpt1  5947  nfmpo  7483  cbvmpox  7494  tfis  7837  fmpox  8046  nfsum1  15632  nfsum  15633  fsum2dlem  15712  fsumcom2  15716  nfcprod  15851  cbvprod  15855  fprod2dlem  15920  fprodcom2  15924  gsum2d2lem  19878  dprd2d2  19951  ptbasfi  23395  restmetu  24389  ovoliunnul  25346  iundisj  25387  iunmbl2  25396  nfitg  25614  limciun  25733  reuxfrdf  32155  abrexss  32173  cbviunf  32211  iunin1f  32213  cbvdisjf  32226  disjabrex  32237  disjabrexf  32238  iundisjf  32244  ssrelf  32268  2ndresdju  32298  fmptcof2  32306  acunirnmpt2f  32310  iundisjfi  32431  fedgmullem2  33160  irngnzply1  33201  locfinreflem  33275  esum2dlem  33545  oms0  33751  bnj1385  34298  bnj900  34395  bnj1014  34427  bnj1123  34452  bnj1228  34477  bnj1321  34493  bnj1384  34498  bnj1398  34500  bnj1408  34502  bnj1444  34509  bnj1445  34510  bnj1446  34511  bnj1449  34514  bnj1467  34520  bnj1518  34530  bj-nfcf  36259  mptsnunlem  36675  phpreu  36928  poimirlem26  36970  mbfposadd  36991  mpobi123f  37486  rababg  42780  ss2iundf  42865  binomcxplemnotnn0  43570  refsumcn  44169  cbvmpo2  44240  cbvmpo1  44241  iinssiin  44272  iinssf  44281  iindif2f  44308  disjrnmpt2  44338  disjinfi  44342  supxrleubrnmptf  44612  limcperiod  44795  limsupequzmptf  44898  dvnprodlem1  45113  stoweidlem16  45183  stoweidlem27  45194  stoweidlem28  45195  stoweidlem29  45196  stoweidlem31  45198  stoweidlem34  45201  stoweidlem35  45202  stoweidlem57  45224  stoweidlem59  45226  stirlinglem5  45245  fourierdlem16  45290  fourierdlem21  45295  fourierdlem22  45296  fourierdlem31  45305  fourierdlem48  45321  fourierdlem51  45324  fourierdlem80  45353  fourierdlem93  45366  etransclem32  45433  smfsupmpt  45982  fsupdm  46009  opeliun2xp  47163  cbvmpox2  47166