Theorem rspceeqv 3634

Description: Restricted existential specialization in an equality, using implicit substitution. (Contributed by BJ, 2-Sep-2022.)

Hypothesis

Ref	Expression
rspceeqv.1	⊢ (𝑥 = 𝐴 → 𝐶 = 𝐷)

Assertion

Ref	Expression
rspceeqv	⊢ ((𝐴 ∈ 𝐵 ∧ 𝐸 = 𝐷) → ∃𝑥 ∈ 𝐵 𝐸 = 𝐶)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝐷   𝑥,𝐸

Allowed substitution hint:   𝐶(𝑥)

Proof of Theorem rspceeqv

Step	Hyp	Ref	Expression
1		rspceeqv.1	. . 3 ⊢ (𝑥 = 𝐴 → 𝐶 = 𝐷)
2	1	eqeq2d 2744	. 2 ⊢ (𝑥 = 𝐴 → (𝐸 = 𝐶 ↔ 𝐸 = 𝐷))
3	2	rspcev 3613	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐸 = 𝐷) → ∃𝑥 ∈ 𝐵 𝐸 = 𝐶)

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107  ∃wrex 3071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072

This theorem is referenced by:  elrnmpt1s  5957  foco2  7109  fcofo  7286  onuninsuci  7829  fo1st  7995  fo2nd  7996  onnseq  8344  nneob  8655  ecelqsg  8766  resixpfo  8930  elixpsn  8931  ixpsnf1o  8932  pwfilem  9177  fofinf1o  9327  pwfilemOLD  9346  elfir  9410  inelfi  9413  fiin  9417  djur  9914  cardalephex  10085  fin23lem38  10344  fin1a2lem11  10405  fin1a2lem13  10407  reclem3pr  11044  infm3lem  12172  ccats1pfxeqrex  14665  2cshwcshw  14776  cshwcshid  14778  cshwcsh2id  14779  shftlem  15015  shftfval  15017  isercoll2  15615  infcvgaux2i  15804  mertenslem1  15830  mertenslem2  15831  fprodser  15893  bezoutlem1  16481  pcprmpw  16816  1arithlem4  16859  vdwapun  16907  vdwlem1  16914  vdwlem2  16915  vdwlem6  16919  vdwlem8  16921  elrestr  17374  gsumwspan  18727  orbsta  19177  psgneldm2i  19373  odf1o2  19441  slwhash  19492  fislw  19493  lsmelvalm  19519  pj1id  19567  efgrelexlemb  19618  cyggeninv  19751  0cyg  19761  eldprdi  19888  lss1d  20574  lspsn  20613  pwssplit1  20670  lspsneq  20735  lspprat  20766  lpi0  20885  lpi1  20886  zringcyg  21039  znf1o  21107  cygznlem3  21125  frgpcyg  21129  islindf4  21393  clsval2  22554  restcld  22676  restcldi  22677  restopnb  22679  restcls  22685  ordtbas2  22695  ordtopn1  22698  ordtopn2  22699  leordtval2  22716  iocpnfordt  22719  icomnfordt  22720  lecldbas  22723  pnrmopn  22847  cncmp  22896  fincmp  22897  cmpsublem  22903  cmpsub  22904  tgcmp  22905  uncmp  22907  cmpfi  22912  connsubclo  22928  2ndcomap  22962  dis2ndc  22964  cldllycmp  22999  dissnlocfin  23033  comppfsc  23036  ptpjopn  23116  txcmplem2  23146  qtopeu  23220  fbasrn  23388  elfm  23451  elfm3  23454  rnelfmlem  23456  rnelfm  23457  fmfnfmlem3  23460  fmfnfmlem4  23461  alexsubALTlem3  23553  ptcmplem2  23557  ptcmplem3  23558  ptcmplem5  23560  tsmsfbas  23632  trust  23734  restutopopn  23743  ustuqtop1  23746  ustuqtop2  23747  ustuqtop4  23749  ustuqtop5  23750  utopsnneiplem  23752  utopsnnei  23754  fmucnd  23797  neipcfilu  23801  mopnex  24028  metrest  24033  metustexhalf  24065  metustfbas  24066  cfilucfil  24068  restmetu  24079  metucn  24080  icoopnst  24455  iocopnst  24456  cnheibor  24471  minveclem2  24943  uniioombllem3  25102  itg1addlem4  25216  itg1addlem4OLD  25217  i1fmulc  25221  ply1lpir  25696  aannenlem2  25842  aalioulem2  25846  eflogeq  26110  cxpeq  26265  angpieqvd  26336  rlimcnp  26470  isppw2  26619  dvdsmulf1o  26698  lgsquadlem1  26883  2sqlem2  26921  mul2sq  26922  2sqlem3  26923  2sqlem9  26930  2sqlem10  26931  ostth2  27140  ostth3  27141  bdayfo  27180  scutfo  27398  addsproplem4  27456  addsproplem5  27457  addsproplem6  27458  addsfo  27467  midexlem  27943  midex  27988  ttgcontlem1  28142  axcontlem7  28228  upgrex  28352  erclwwlkref  29273  clwwlkfo  29303  erclwwlknref  29322  isgrpo  29750  grpoinvf  29785  minvecolem2  30128  shsel3  30568  pjhthlem2  30645  h1de2ctlem  30808  spansncol  30821  superpos  31607  cdj3lem2  31688  wrdsplex  32104  archiabllem1a  32337  archiabllem1b  32338  cmpcref  32830  ordtconnlem1  32904  gsumesum  33057  esumcst  33061  esumpcvgval  33076  sxbrsigalem2  33285  oms0  33296  omssubadd  33299  eulerpartlemt  33370  cvmsss2  34265  cvmfolem  34270  fobigcup  34872  opnregcld  35215  cldregopn  35216  onsucsuccmpi  35328  finixpnum  36473  poimirlem16  36504  poimirlem19  36507  itg2addnclem2  36540  isbnd2  36651  isbnd3  36652  totbndbnd  36657  heibor1lem  36677  heibor  36689  rngmgmbs4  36799  prnc  36935  prtlem11  37736  lsatlspsn2  37862  lsatlspsn  37863  lfl1dim  37991  lfl1dim2N  37992  lkrss2N  38039  glbconN  38247  glbconNOLD  38248  atpointN  38614  ispsubcl2N  38818  dihglblem2aN  40164  dihglblem2N  40165  dihatexv  40209  dvh4dimat  40309  dochfl1  40347  lcfl8  40373  lcfrlem9  40421  mapdval2N  40501  mapdval4N  40503  mapdcv  40531  mapdspex  40539  hdmap14lem2a  40738  hdmap14lem6  40744  elrfi  41432  eldioph  41496  eldioph2b  41501  eldioph3  41504  eldioph4i  41550  rencldnfilem  41558  pellfund14  41636  rmxyelqirr  41648  rmxyelqirrOLD  41649  filnm  41832  unxpwdom3  41837  lpirlnr  41859  hbt  41872  rngunsnply  41915  ofoafo  42106  naddcnffo  42114  oaun3lem1  42124  dvconstbi  43093  elrestd  43797  wessf1ornlem  43882  iccshift  44231  iooshift  44235  limcperiod  44344  sumnnodd  44346  dvnprodlem1  44662  itgperiod  44697  stirlinglem13  44802  sge0rnn0  45084  sge00  45092  fsumlesge0  45093  sge0tsms  45096  sge0cl  45097  sge0f1o  45098  sge0sup  45107  sge0resplit  45122  sge0xaddlem2  45150  sge0reuz  45163  sge0reuzb  45164  nnfoctbdjlem  45171  ovn0lem  45281  hoidmv1le  45310  hoidmvlelem1  45311  incsmflem  45457  decsmflem  45482  sigarcol  45580  7gbow  46440  0aryfvalel  47320  iscnrm3rlem2  47574