Theorem nfcri 2919

Description: Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.) Avoid ax-10 2179, ax-11 2195. (Revised by GG, 23-May-2024.) Avoid ax-12 2216 (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 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴

This proof depends on syntax axioms:  Ⅎwnf 1816   ∈ wcel 2146  Ⅎwnfc 2912

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-nf 1817  df-clel 2840  df-nfc 2914

This theorem is used by:  nfcrii  2922  clelsb1fw  2931  clelsb1f  2932  cleqf  2955  sbabel  2959  r2alf  3288  cbvralfw  3307  cbvralf  3351  nfrmow  3400  nfreuw  3401  cbvrabw  3453  nfrabw  3454  nfrab  3455  cbvrab  3456  rmo3f  3699  nfccdeq  3743  sbcabel  3832  cbvcsbw  3864  cbvcsb  3865  csbgfi  3874  cbvrabcsfw  3895  cbvralcsf  3896  cbvreucsf  3898  cbvrabcsf  3899  dfssf  3929  nfdif  4084  nfun  4124  nfin  4177  nfiun  4990  nfiin  4991  nfiung  4992  nfiing  4993  cbviun  5001  cbviin  5002  cbviung  5003  cbviing  5004  iunssf  5009  iunssfOLD  5010  iunxsngf  5060  cbvdisj  5088  nfdisjw  5090  nfdisj  5091  nfmpt  5211  cbvmptf  5213  cbvmptfg  5214  reusv2lem4  5374  nfxp  5696  opeliunxp  5730  opeliun2xp  5731  iunxpf  5836  elrnmpt1  5952  nfmpo  7498  cbvmpox  7509  tfis  7853  fmpox  8066  nfsum1  15760  nfsum  15761  fsum2dlem  15839  fsumcom2  15843  nfcprod  15981  cbvprod  15985  fprod2dlem  16052  fprodcom2  16056  gsum2d2lem  20066  dprd2d2  20139  ptbasfi  23767  restmetu  24756  ovoliunnul  25695  iundisj  25736  iunmbl2  25745  nfitg  25963  limciun  26082  reuxfrdf  32866  abrexss  32887  cbviunf  32929  iunin1f  32931  cbvdisjf  32945  disjabrex  32956  disjabrexf  32957  iundisjf  32963  ssrelf  32989  2ndresdju  33023  fmptcof2  33031  acunirnmpt2f  33035  iundisjfi  33170  suppgsumssiun  33415  fedgmullem2  34043  irngnzply1  34104  locfinreflem  34253  esum2dlem  34505  oms0  34711  bnj1385  35244  bnj900  35341  bnj1014  35373  bnj1123  35398  bnj1228  35423  bnj1321  35439  bnj1384  35444  bnj1398  35446  bnj1408  35448  bnj1444  35455  bnj1445  35456  bnj1446  35457  bnj1449  35460  bnj1467  35466  bnj1518  35476  bj-nfcf  37591  mptsnunlem  38017  phpreu  38288  poimirlem26  38330  mbfposadd  38351  mpobi123f  38844  rababg  44333  ss2iundf  44418  binomcxplemnotnn0  45099  refsumcn  45783  cbvmpo2  45848  cbvmpo1  45849  iinssiin  45880  iinssf  45889  iindif2f  45911  disjrnmpt2  45939  disjinfi  45943  supxrleubrnmptf  46198  limcperiod  46377  limsupequzmptf  46478  dvnprodlem1  46693  stoweidlem16  46763  stoweidlem27  46774  stoweidlem28  46775  stoweidlem29  46776  stoweidlem31  46778  stoweidlem34  46781  stoweidlem35  46782  stoweidlem57  46804  stoweidlem59  46806  stirlinglem5  46825  fourierdlem16  46870  fourierdlem21  46875  fourierdlem22  46876  fourierdlem31  46885  fourierdlem48  46901  fourierdlem51  46904  fourierdlem80  46933  fourierdlem93  46946  etransclem32  47013  smfsupmpt  47562  smfinfmpt  47566  fsupdm  47589  cbvmpox2  49149  iinfssc  49868  iinfsubc  49869