Theorem nfcri 2891

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

Syntax hints:  Ⅎwnf 1785   ∈ wcel 2114  Ⅎwnfc 2884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-nf 1786  df-clel 2812  df-nfc 2886

This theorem is referenced by:  nfcrii  2894  clelsb1fw  2903  clelsb1f  2904  cleqf  2928  sbabel  2932  r2alf  3259  cbvralfw  3278  cbvralf  3323  nfrmow  3372  nfreuw  3373  cbvrabw  3425  cbvrabwOLD  3426  nfrabw  3427  nfrab  3428  cbvrab  3429  rmo3f  3681  nfccdeq  3725  sbcabel  3817  cbvcsbw  3848  cbvcsb  3849  csbgfi  3858  cbvrabcsfw  3879  cbvralcsf  3880  cbvreucsf  3882  cbvrabcsf  3883  dfssf  3913  nfdif  4070  nfdifOLD  4071  nfun  4111  nfunOLD  4112  nfin  4165  nfinOLD  4166  nfiun  4966  nfiin  4967  nfiung  4968  nfiing  4969  cbviun  4978  cbviin  4979  cbviung  4980  cbviing  4981  iunssf  4986  iunssfOLD  4987  iunxsngf  5035  cbvdisj  5063  nfdisjw  5065  nfdisj  5066  nfmpt  5184  cbvmptf  5186  cbvmptfg  5187  reusv2lem4  5338  nfxp  5657  opeliunxp  5691  opeliun2xp  5692  iunxpf  5797  elrnmpt1  5909  nfmpo  7442  cbvmpox  7453  tfis  7799  fmpox  8013  nfsum1  15643  nfsum  15644  fsum2dlem  15723  fsumcom2  15727  nfcprod  15865  cbvprod  15869  fprod2dlem  15936  fprodcom2  15940  gsum2d2lem  19939  dprd2d2  20012  ptbasfi  23556  restmetu  24545  ovoliunnul  25484  iundisj  25525  iunmbl2  25534  nfitg  25752  limciun  25871  reuxfrdf  32575  abrexss  32597  cbviunf  32640  iunin1f  32642  cbvdisjf  32656  disjabrex  32667  disjabrexf  32668  iundisjf  32674  ssrelf  32703  2ndresdju  32737  fmptcof2  32745  acunirnmpt2f  32749  iundisjfi  32884  suppgsumssiun  33148  fedgmullem2  33790  irngnzply1  33851  locfinreflem  34000  esum2dlem  34252  oms0  34457  bnj1385  34990  bnj900  35087  bnj1014  35119  bnj1123  35144  bnj1228  35169  bnj1321  35185  bnj1384  35190  bnj1398  35192  bnj1408  35194  bnj1444  35201  bnj1445  35202  bnj1446  35203  bnj1449  35206  bnj1467  35212  bnj1518  35222  bj-nfcf  37246  mptsnunlem  37668  phpreu  37939  poimirlem26  37981  mbfposadd  38002  mpobi123f  38497  rababg  44019  ss2iundf  44104  binomcxplemnotnn0  44801  refsumcn  45479  cbvmpo2  45545  cbvmpo1  45546  iinssiin  45577  iinssf  45586  iindif2f  45608  disjrnmpt2  45636  disjinfi  45640  supxrleubrnmptf  45897  limcperiod  46076  limsupequzmptf  46177  dvnprodlem1  46392  stoweidlem16  46462  stoweidlem27  46473  stoweidlem28  46474  stoweidlem29  46475  stoweidlem31  46477  stoweidlem34  46480  stoweidlem35  46481  stoweidlem57  46503  stoweidlem59  46505  stirlinglem5  46524  fourierdlem16  46569  fourierdlem21  46574  fourierdlem22  46575  fourierdlem31  46584  fourierdlem48  46600  fourierdlem51  46603  fourierdlem80  46632  fourierdlem93  46645  etransclem32  46712  smfsupmpt  47261  smfinfmpt  47265  fsupdm  47288  cbvmpox2  48824  iinfssc  49544  iinfsubc  49545