Theorem rspceeqv 3608

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 2740	. 2 ⊢ (𝑥 = 𝐴 → (𝐸 = 𝐶 ↔ 𝐸 = 𝐷))
3	2	rspcev 3585	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐸 = 𝐷) → ∃𝑥 ∈ 𝐵 𝐸 = 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054

This theorem is referenced by:  elrnmpt1s  5912  foco2  7063  fcofo  7245  onuninsuci  7796  fo1st  7967  fo2nd  7968  onnseq  8290  nneob  8597  ecelqs  8718  resixpfo  8886  elixpsn  8887  ixpsnf1o  8888  pwfilem  9243  fofinf1o  9259  elfir  9342  inelfi  9345  fiin  9349  djur  9848  cardalephex  10019  fin23lem38  10278  fin1a2lem11  10339  fin1a2lem13  10341  reclem3pr  10978  infm3lem  12117  ccats1pfxeqrex  14656  2cshwcshw  14767  cshwcshid  14769  cshwcsh2id  14770  shftlem  15010  shftfval  15012  isercoll2  15611  infcvgaux2i  15800  mertenslem1  15826  mertenslem2  15827  fprodser  15891  bezoutlem1  16485  pcprmpw  16830  1arithlem4  16873  vdwapun  16921  vdwlem1  16928  vdwlem2  16929  vdwlem6  16933  vdwlem8  16935  elrestr  17367  gsumwspan  18749  orbsta  19221  psgneldm2i  19411  odf1o2  19479  slwhash  19530  fislw  19531  lsmelvalm  19557  pj1id  19605  efgrelexlemb  19656  cyggeninv  19789  0cyg  19799  eldprdi  19926  lss1d  20845  lspsn  20884  pwssplit1  20942  lspsneq  21008  lspprat  21039  lpi0  21212  lpi1  21213  zringcyg  21355  znf1o  21437  cygznlem3  21455  frgpcyg  21459  islindf4  21723  clsval2  22913  restcld  23035  restcldi  23036  restopnb  23038  restcls  23044  ordtbas2  23054  ordtopn1  23057  ordtopn2  23058  leordtval2  23075  iocpnfordt  23078  icomnfordt  23079  lecldbas  23082  pnrmopn  23206  cncmp  23255  fincmp  23256  cmpsublem  23262  cmpsub  23263  tgcmp  23264  uncmp  23266  cmpfi  23271  connsubclo  23287  2ndcomap  23321  dis2ndc  23323  cldllycmp  23358  dissnlocfin  23392  comppfsc  23395  ptpjopn  23475  txcmplem2  23505  qtopeu  23579  fbasrn  23747  elfm  23810  elfm3  23813  rnelfmlem  23815  rnelfm  23816  fmfnfmlem3  23819  fmfnfmlem4  23820  alexsubALTlem3  23912  ptcmplem2  23916  ptcmplem3  23917  ptcmplem5  23919  tsmsfbas  23991  trust  24093  restutopopn  24102  ustuqtop1  24105  ustuqtop2  24106  ustuqtop4  24108  ustuqtop5  24109  utopsnneiplem  24111  utopsnnei  24113  fmucnd  24155  neipcfilu  24159  mopnex  24383  metrest  24388  metustexhalf  24420  metustfbas  24421  cfilucfil  24423  restmetu  24434  metucn  24435  icoopnst  24812  iocopnst  24813  cnheibor  24830  minveclem2  25302  uniioombllem3  25462  itg1addlem4  25576  i1fmulc  25580  ply1lpir  26063  aannenlem2  26213  aalioulem2  26217  eflogeq  26487  cxpeq  26643  angpieqvd  26717  rlimcnp  26851  isppw2  27001  mpodvdsmulf1o  27080  dvdsmulf1o  27082  lgsquadlem1  27267  2sqlem2  27305  mul2sq  27306  2sqlem3  27307  2sqlem9  27314  2sqlem10  27315  ostth2  27524  ostth3  27525  bdayfo  27565  scutfo  27792  addsproplem4  27855  addsproplem5  27856  addsproplem6  27857  addsfo  27866  subsfo  27945  elons2  28135  n0seo  28283  zseo  28284  midexlem  28595  midex  28640  ttgcontlem1  28788  axcontlem7  28873  upgrex  28995  erclwwlkref  29922  clwwlkfo  29952  erclwwlknref  29971  isgrpo  30399  grpoinvf  30434  minvecolem2  30777  shsel3  31217  pjhthlem2  31294  h1de2ctlem  31457  spansncol  31470  superpos  32256  cdj3lem2  32337  wrdsplex  32830  archiabllem1a  33118  archiabllem1b  33119  cmpcref  33813  ordtconnlem1  33887  gsumesum  34022  esumcst  34026  esumpcvgval  34041  sxbrsigalem2  34250  oms0  34261  omssubadd  34264  eulerpartlemt  34335  cvmsss2  35234  cvmfolem  35239  fobigcup  35861  opnregcld  36291  cldregopn  36292  onsucsuccmpi  36404  finixpnum  37572  poimirlem16  37603  poimirlem19  37606  itg2addnclem2  37639  isbnd2  37750  isbnd3  37751  totbndbnd  37756  heibor1lem  37776  heibor  37788  rngmgmbs4  37898  prnc  38034  prtlem11  38832  lsatlspsn2  38958  lsatlspsn  38959  lfl1dim  39087  lfl1dim2N  39088  lkrss2N  39135  glbconN  39343  glbconNOLD  39344  atpointN  39710  ispsubcl2N  39914  dihglblem2aN  41260  dihglblem2N  41261  dihatexv  41305  dvh4dimat  41405  dochfl1  41443  lcfl8  41469  lcfrlem9  41517  mapdval2N  41597  mapdval4N  41599  mapdcv  41627  mapdspex  41635  hdmap14lem2a  41834  hdmap14lem6  41840  elrfi  42655  eldioph  42719  eldioph2b  42724  eldioph3  42727  eldioph4i  42773  rencldnfilem  42781  pellfund14  42859  rmxyelqirr  42871  rmxyelqirrOLD  42872  filnm  43052  unxpwdom3  43057  lpirlnr  43079  hbt  43092  rngunsnply  43131  ofoafo  43318  naddcnffo  43326  oaun3lem1  43336  dvconstbi  44296  elrestd  45075  wessf1ornlem  45152  iccshift  45489  iooshift  45493  limcperiod  45599  sumnnodd  45601  dvnprodlem1  45917  itgperiod  45952  stirlinglem13  46057  sge0rnn0  46339  sge00  46347  fsumlesge0  46348  sge0tsms  46351  sge0cl  46352  sge0f1o  46353  sge0sup  46362  sge0resplit  46377  sge0xaddlem2  46405  sge0reuz  46418  sge0reuzb  46419  nnfoctbdjlem  46426  ovn0lem  46536  hoidmv1le  46565  hoidmvlelem1  46566  incsmflem  46712  decsmflem  46737  sigarcol  46835  7gbow  47746  0aryfvalel  48596  iscnrm3rlem2  48902