Theorem nfcri 2893

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

Syntax hints:  Ⅎwnf 1787   ∈ wcel 2108  Ⅎwnfc 2886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-nf 1788  df-clel 2817  df-nfc 2888

This theorem is referenced by:  nfcrii  2898  nfcriiOLD  2899  clelsb1fw  2910  clelsb1f  2911  cleqf  2937  sbabel  2940  sbabelOLD  2941  r2alf  3145  nfrabw  3311  nfrab  3312  cbvralfw  3358  cbvralfwOLD  3359  cbvralf  3361  cbvrabw  3414  cbvrab  3415  rmo3f  3664  nfccdeq  3708  sbcabel  3807  cbvcsbw  3838  cbvcsb  3839  csbgfi  3849  cbvrabcsfw  3872  cbvralcsf  3873  cbvreucsf  3875  cbvrabcsf  3876  dfss2f  3907  nfdif  4056  nfun  4095  nfin  4147  nfiun  4951  nfiin  4952  nfiung  4953  nfiing  4954  cbviun  4962  cbviin  4963  cbviung  4964  cbviing  4965  iunssf  4970  iunxsngf  5017  cbvdisj  5045  nfdisjw  5047  nfdisj  5048  nfmpt  5177  cbvmptf  5179  cbvmptfg  5180  reusv2lem4  5319  nfxp  5613  opeliunxp  5645  iunxpf  5746  elrnmpt1  5856  nfmpo  7335  cbvmpox  7346  tfis  7676  fmpox  7880  nfsum1  15329  nfsum  15330  nfsumOLD  15331  fsum2dlem  15410  fsumcom2  15414  nfcprod  15549  cbvprod  15553  fprod2dlem  15618  fprodcom2  15622  gsum2d2lem  19489  dprd2d2  19562  ptbasfi  22640  restmetu  23632  ovoliunnul  24576  iundisj  24617  iunmbl2  24626  nfitg  24844  limciun  24963  reuxfrdf  30740  abrexss  30758  cbviunf  30796  iunin1f  30798  cbvdisjf  30811  disjabrex  30822  disjabrexf  30823  iundisjf  30829  ssrelf  30856  2ndresdju  30887  fmptcof2  30896  acunirnmpt2f  30900  iundisjfi  31019  fedgmullem2  31613  locfinreflem  31692  esum2dlem  31960  oms0  32164  bnj1385  32712  bnj900  32809  bnj1014  32841  bnj1123  32866  bnj1228  32891  bnj1321  32907  bnj1384  32912  bnj1398  32914  bnj1408  32916  bnj1444  32923  bnj1445  32924  bnj1446  32925  bnj1449  32928  bnj1467  32934  bnj1518  32944  bj-nfcf  35038  mptsnunlem  35436  phpreu  35688  poimirlem26  35730  mbfposadd  35751  mpobi123f  36247  rababg  41070  ss2iundf  41156  binomcxplemnotnn0  41863  refsumcn  42462  cbvmpo2  42536  cbvmpo1  42537  iinssiin  42567  iinssf  42576  disjrnmpt2  42615  disjinfi  42620  supxrleubrnmptf  42881  limcperiod  43059  limsupequzmptf  43162  dvnprodlem1  43377  stoweidlem16  43447  stoweidlem27  43458  stoweidlem28  43459  stoweidlem29  43460  stoweidlem31  43462  stoweidlem34  43465  stoweidlem35  43466  stoweidlem57  43488  stoweidlem59  43490  stirlinglem5  43509  fourierdlem16  43554  fourierdlem21  43559  fourierdlem22  43560  fourierdlem31  43569  fourierdlem48  43585  fourierdlem51  43588  fourierdlem80  43617  fourierdlem93  43630  etransclem32  43697  smfsupmpt  44235  opeliun2xp  45556  cbvmpox2  45559