Theorem nfcri 2918

Description: Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.) Avoid ax-10 2180, ax-11 2197. (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 2916	. 2 ⊢ (Ⅎ𝑥𝐴 → Ⅎ𝑥 𝑦 ∈ 𝐴)
3	1, 2	ax-mp 5	1 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴

This proof depends on syntax axioms:  Ⅎwnf 1816   ∈ wcel 2147  Ⅎwnfc 2911

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 1945  ax-6 2002  ax-7 2043  ax-8 2149

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

This theorem is used by:  nfcrii  2921  clelsb1fw  2930  clelsb1f  2931  cleqf  2954  sbabel  2958  r2alf  3287  cbvralfw  3306  cbvralf  3349  nfrmow  3398  nfreuw  3399  cbvrabw  3450  nfrabw  3451  nfrab  3452  cbvrab  3453  rmo3f  3695  nfccdeq  3739  sbcabel  3829  cbvcsbw  3861  cbvcsb  3862  csbgfi  3871  cbvrabcsfw  3892  cbvralcsf  3893  cbvreucsf  3895  cbvrabcsf  3896  dfssf  3904  nfdif  4069  nfin  4124  nfun  4172  nfiun  4987  nfiin  4988  nfiung  4989  nfiing  4990  cbviun  4998  cbviin  4999  cbviung  5000  cbviing  5001  iunssf  5006  iunssfOLD  5007  iunxsngf  5057  cbvdisj  5085  nfdisjw  5087  nfdisj  5088  nfmpt  5209  cbvmptf  5211  cbvmptfg  5212  reusv2lem4  5370  nfxp  5691  opeliunxp  5725  opeliun2xp  5726  iunxpf  5836  elrnmpt1  5954  nfmpo  7533  cbvmpox  7544  tfis  7900  fmpox  8113  nfsum1  15901  nfsum  15902  fsum2dlem  15980  fsumcom2  15984  nfcprod  16122  cbvprod  16126  fprod2dlem  16191  fprodcom2  16195  gsum2d2lem  20238  dprd2d2  20311  ptbasfi  23955  restmetu  24944  ovoliunnul  25883  iundisj  25924  iunmbl2  25933  nfitg  26150  limciun  26269  reuxfrdf  33186  abrexss  33207  cbviunf  33248  iunin1f  33250  cbvdisjf  33263  disjabrex  33274  disjabrexf  33275  iundisjf  33281  ssrelf  33307  2ndresdju  33341  fmptcof2  33349  acunirnmpt2  33352  acunirnmpt2f  33353  iundisjfi  33484  suppgsumssiun  33732  fedgmullem2  34373  irngnzply1  34434  locfinreflem  34583  esum2dlem  34835  oms0  35040  bnj1385  35573  bnj900  35670  bnj1014  35702  bnj1123  35727  bnj1228  35752  bnj1321  35768  bnj1384  35773  bnj1398  35775  bnj1408  35777  bnj1444  35784  bnj1445  35785  bnj1446  35786  bnj1449  35789  bnj1467  35795  bnj1518  35805  srepdflem1  36126  bj-nfcf  38050  mptsnunlem  38529  phpreu  38795  poimirlem26  38832  mbfposadd  38853  mpobi123f  39360  rababg  44836  ss2iundf  44920  binomcxplemnotnn0  45601  refsumcn  46321  cbvmpo2  46385  cbvmpo1  46386  iinssiin  46417  iinssf  46426  iindif2f  46448  disjrnmpt2  46476  disjinfi  46480  supxrleubrnmptf  46734  limcperiod  46913  limsupequzmptf  47014  dvnprodlem1  47229  stoweidlem16  47299  stoweidlem27  47310  stoweidlem28  47311  stoweidlem29  47312  stoweidlem31  47314  stoweidlem34  47317  stoweidlem35  47318  stoweidlem57  47340  stoweidlem59  47342  stirlinglem5  47361  fourierdlem16  47406  fourierdlem21  47411  fourierdlem22  47412  fourierdlem31  47421  fourierdlem48  47437  fourierdlem51  47440  fourierdlem80  47469  fourierdlem93  47482  etransclem32  47549  smfsupmpt  48098  smfinfmpt  48102  fsupdm  48125  cbvmpox2  49779  iinfssc  50502  iinfsubc  50503