Theorem nfcri 2919

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

Syntax hints:  Ⅎwnf 1806   ∈ wcel 2145  Ⅎwnfc 2912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-nf 1807  df-clel 2840  df-nfc 2914

This theorem is referenced by:  nfcrii  2922  clelsb1fw  2931  clelsb1f  2932  cleqf  2955  sbabel  2959  r2alf  3286  cbvralfw  3305  cbvralf  3350  nfrmow  3399  nfreuw  3400  cbvrabw  3452  cbvrabwOLD  3453  nfrabw  3454  nfrab  3455  cbvrab  3456  rmo3f  3700  nfccdeq  3744  sbcabel  3834  cbvcsbw  3865  cbvcsb  3866  csbgfi  3875  cbvrabcsfw  3896  cbvralcsf  3897  cbvreucsf  3899  cbvrabcsf  3900  dfssf  3930  nfdif  4086  nfun  4126  nfin  4179  nfiun  4983  nfiin  4984  nfiung  4985  nfiing  4986  cbviun  4994  cbviin  4995  cbviung  4996  cbviing  4997  iunssf  5002  iunssfOLD  5003  iunxsngf  5053  cbvdisj  5081  nfdisjw  5083  nfdisj  5084  nfmpt  5202  cbvmptf  5204  cbvmptfg  5205  reusv2lem4  5362  nfxp  5684  opeliunxp  5718  opeliun2xp  5719  iunxpf  5824  elrnmpt1  5940  nfmpo  7482  cbvmpox  7493  tfis  7839  fmpox  8052  nfsum1  15729  nfsum  15730  fsum2dlem  15809  fsumcom2  15813  nfcprod  15951  cbvprod  15955  fprod2dlem  16022  fprodcom2  16026  gsum2d2lem  20031  dprd2d2  20104  ptbasfi  23695  restmetu  24684  ovoliunnul  25623  iundisj  25664  iunmbl2  25673  nfitg  25891  limciun  26010  reuxfrdf  32743  abrexss  32764  cbviunf  32806  iunin1f  32808  cbvdisjf  32822  disjabrex  32833  disjabrexf  32834  iundisjf  32840  ssrelf  32868  2ndresdju  32902  fmptcof2  32910  acunirnmpt2f  32914  iundisjfi  33049  suppgsumssiun  33300  fedgmullem2  33932  irngnzply1  33993  locfinreflem  34142  esum2dlem  34394  oms0  34599  bnj1385  35132  bnj900  35229  bnj1014  35261  bnj1123  35286  bnj1228  35311  bnj1321  35327  bnj1384  35332  bnj1398  35334  bnj1408  35336  bnj1444  35343  bnj1445  35344  bnj1446  35345  bnj1449  35348  bnj1467  35354  bnj1518  35364  bj-nfcf  37415  mptsnunlem  37839  phpreu  38110  poimirlem26  38152  mbfposadd  38173  mpobi123f  38668  rababg  44157  ss2iundf  44242  binomcxplemnotnn0  44925  refsumcn  45609  cbvmpo2  45674  cbvmpo1  45675  iinssiin  45706  iinssf  45715  iindif2f  45737  disjrnmpt2  45765  disjinfi  45769  supxrleubrnmptf  46024  limcperiod  46203  limsupequzmptf  46304  dvnprodlem1  46519  stoweidlem16  46589  stoweidlem27  46600  stoweidlem28  46601  stoweidlem29  46602  stoweidlem31  46604  stoweidlem34  46607  stoweidlem35  46608  stoweidlem57  46630  stoweidlem59  46632  stirlinglem5  46651  fourierdlem16  46696  fourierdlem21  46701  fourierdlem22  46702  fourierdlem31  46711  fourierdlem48  46727  fourierdlem51  46730  fourierdlem80  46759  fourierdlem93  46772  etransclem32  46839  smfsupmpt  47388  smfinfmpt  47392  fsupdm  47415  cbvmpox2  48968  iinfssc  49687  iinfsubc  49688