Theorem nfcri 2900

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

Syntax hints:  Ⅎwnf 1781   ∈ wcel 2108  Ⅎwnfc 2893

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-nf 1782  df-clel 2819  df-nfc 2895

This theorem is referenced by:  nfcrii  2903  clelsb1fw  2912  clelsb1f  2913  cleqf  2940  sbabel  2944  sbabelOLD  2945  r2alf  3287  cbvralfw  3310  nfralw  3317  cbvralf  3368  nfrmow  3421  nfreuw  3422  cbvrabw  3481  cbvrabwOLD  3482  nfrabw  3483  nfrabwOLD  3484  nfrab  3486  cbvrab  3487  rmo3f  3756  nfccdeq  3800  sbcabel  3900  cbvcsbw  3931  cbvcsb  3932  csbgfi  3942  cbvrabcsfw  3965  cbvralcsf  3966  cbvreucsf  3968  cbvrabcsf  3969  dfssf  3999  nfdif  4152  nfdifOLD  4153  nfun  4193  nfunOLD  4194  nfin  4245  nfinOLD  4246  nfiun  5046  nfiin  5047  nfiung  5048  nfiing  5049  cbviun  5059  cbviin  5060  cbviung  5061  cbviing  5062  iunssf  5067  iunxsngf  5115  cbvdisj  5143  nfdisjw  5145  nfdisj  5146  nfmpt  5273  cbvmptf  5275  cbvmptfg  5276  reusv2lem4  5419  nfxp  5733  opeliunxp  5767  iunxpf  5873  elrnmpt1  5983  nfmpo  7532  cbvmpox  7543  tfis  7892  fmpox  8108  nfsum1  15738  nfsum  15739  fsum2dlem  15818  fsumcom2  15822  nfcprod  15957  cbvprod  15961  fprod2dlem  16028  fprodcom2  16032  gsum2d2lem  20015  dprd2d2  20088  ptbasfi  23610  restmetu  24604  ovoliunnul  25561  iundisj  25602  iunmbl2  25611  nfitg  25830  limciun  25949  reuxfrdf  32519  abrexss  32540  cbviunf  32578  iunin1f  32580  cbvdisjf  32593  disjabrex  32604  disjabrexf  32605  iundisjf  32611  ssrelf  32637  2ndresdju  32667  fmptcof2  32675  acunirnmpt2f  32679  iundisjfi  32801  fedgmullem2  33643  irngnzply1  33691  locfinreflem  33786  esum2dlem  34056  oms0  34262  bnj1385  34808  bnj900  34905  bnj1014  34937  bnj1123  34962  bnj1228  34987  bnj1321  35003  bnj1384  35008  bnj1398  35010  bnj1408  35012  bnj1444  35019  bnj1445  35020  bnj1446  35021  bnj1449  35024  bnj1467  35030  bnj1518  35040  bj-nfcf  36889  mptsnunlem  37304  phpreu  37564  poimirlem26  37606  mbfposadd  37627  mpobi123f  38122  rababg  43536  ss2iundf  43621  binomcxplemnotnn0  44325  refsumcn  44930  cbvmpo2  44999  cbvmpo1  45000  iinssiin  45031  iinssf  45040  iindif2f  45065  disjrnmpt2  45095  disjinfi  45099  supxrleubrnmptf  45366  limcperiod  45549  limsupequzmptf  45652  dvnprodlem1  45867  stoweidlem16  45937  stoweidlem27  45948  stoweidlem28  45949  stoweidlem29  45950  stoweidlem31  45952  stoweidlem34  45955  stoweidlem35  45956  stoweidlem57  45978  stoweidlem59  45980  stirlinglem5  45999  fourierdlem16  46044  fourierdlem21  46049  fourierdlem22  46050  fourierdlem31  46059  fourierdlem48  46075  fourierdlem51  46078  fourierdlem80  46107  fourierdlem93  46120  etransclem32  46187  smfsupmpt  46736  fsupdm  46763  opeliun2xp  48057  cbvmpox2  48060