Theorem nfcri 2914

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

This proof depends on syntax axioms:  Ⅎwnf 1815   ∈ wcel 2144  Ⅎwnfc 2907

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-nf 1816  df-clel 2835  df-nfc 2909

This theorem is used by:  nfcrii  2917  clelsb1fw  2926  clelsb1f  2927  cleqf  2950  sbabel  2954  r2alf  3283  cbvralfw  3302  cbvralf  3345  nfrmow  3394  nfreuw  3395  cbvrabw  3446  nfrabw  3447  nfrab  3448  cbvrab  3449  rmo3f  3691  nfccdeq  3735  sbcabel  3824  cbvcsbw  3856  cbvcsb  3857  csbgfi  3866  cbvrabcsfw  3887  cbvralcsf  3888  cbvreucsf  3890  cbvrabcsf  3891  dfssf  3899  nfdif  4066  nfin  4121  nfun  4169  nfiun  4981  nfiin  4982  nfiung  4983  nfiing  4984  cbviun  4992  cbviin  4993  cbviung  4994  cbviing  4995  iunssf  5000  iunssfOLD  5001  iunxsngf  5051  cbvdisj  5079  nfdisjw  5081  nfdisj  5082  nfmpt  5202  cbvmptf  5204  cbvmptfg  5205  reusv2lem4  5362  nfxp  5683  opeliunxp  5717  opeliun2xp  5718  iunxpf  5825  elrnmpt1  5941  nfmpo  7503  cbvmpox  7514  tfis  7867  fmpox  8079  nfsum1  15863  nfsum  15864  fsum2dlem  15942  fsumcom2  15946  nfcprod  16084  cbvprod  16088  fprod2dlem  16153  fprodcom2  16157  gsum2d2lem  20193  dprd2d2  20266  ptbasfi  23906  restmetu  24895  ovoliunnul  25834  iundisj  25875  iunmbl2  25884  nfitg  26101  limciun  26220  reuxfrdf  33135  abrexss  33156  cbviunf  33198  iunin1f  33200  cbvdisjf  33213  disjabrex  33224  disjabrexf  33225  iundisjf  33231  ssrelf  33257  2ndresdju  33291  fmptcof2  33299  acunirnmpt2  33302  acunirnmpt2f  33303  iundisjfi  33435  suppgsumssiun  33680  fedgmullem2  34309  irngnzply1  34370  locfinreflem  34519  esum2dlem  34771  oms0  34976  bnj1385  35509  bnj900  35606  bnj1014  35638  bnj1123  35663  bnj1228  35688  bnj1321  35704  bnj1384  35709  bnj1398  35711  bnj1408  35713  bnj1444  35720  bnj1445  35721  bnj1446  35722  bnj1449  35725  bnj1467  35731  bnj1518  35741  srepdflem1  36005  bj-nfcf  37928  mptsnunlem  38355  phpreu  38621  poimirlem26  38658  mbfposadd  38679  mpobi123f  39188  rababg  44669  ss2iundf  44753  binomcxplemnotnn0  45434  refsumcn  46141  cbvmpo2  46206  cbvmpo1  46207  iinssiin  46238  iinssf  46247  iindif2f  46269  disjrnmpt2  46297  disjinfi  46301  supxrleubrnmptf  46555  limcperiod  46734  limsupequzmptf  46835  dvnprodlem1  47050  stoweidlem16  47120  stoweidlem27  47131  stoweidlem28  47132  stoweidlem29  47133  stoweidlem31  47135  stoweidlem34  47138  stoweidlem35  47139  stoweidlem57  47161  stoweidlem59  47163  stirlinglem5  47182  fourierdlem16  47227  fourierdlem21  47232  fourierdlem22  47233  fourierdlem31  47242  fourierdlem48  47258  fourierdlem51  47261  fourierdlem80  47290  fourierdlem93  47303  etransclem32  47370  smfsupmpt  47919  smfinfmpt  47923  fsupdm  47946  cbvmpox2  49542  iinfssc  50265  iinfsubc  50266