Theorem rspceeqv 3599

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ∃wrex 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061

This theorem is referenced by:  elrnmpt1s  5908  foco2  7054  fcofo  7234  onuninsuci  7782  fo1st  7953  fo2nd  7954  onnseq  8276  nneob  8584  ecelqs  8705  resixpfo  8874  elixpsn  8875  ixpsnf1o  8876  pwfilem  9218  fofinf1o  9232  elfir  9318  inelfi  9321  fiin  9325  djur  9831  cardalephex  10000  fin23lem38  10259  fin1a2lem11  10320  fin1a2lem13  10322  reclem3pr  10960  infm3lem  12100  ccats1pfxeqrex  14638  2cshwcshw  14748  cshwcshid  14750  cshwcsh2id  14751  shftlem  14991  shftfval  14993  isercoll2  15592  infcvgaux2i  15781  mertenslem1  15807  mertenslem2  15808  fprodser  15872  bezoutlem1  16466  pcprmpw  16811  1arithlem4  16854  vdwapun  16902  vdwlem1  16909  vdwlem2  16910  vdwlem6  16914  vdwlem8  16916  elrestr  17348  gsumwspan  18771  orbsta  19242  psgneldm2i  19434  odf1o2  19502  slwhash  19553  fislw  19554  lsmelvalm  19580  pj1id  19628  efgrelexlemb  19679  cyggeninv  19812  0cyg  19822  eldprdi  19949  lss1d  20914  lspsn  20953  pwssplit1  21011  lspsneq  21077  lspprat  21108  lpi0  21281  lpi1  21282  zringcyg  21424  znf1o  21506  cygznlem3  21524  frgpcyg  21528  islindf4  21793  clsval2  22994  restcld  23116  restcldi  23117  restopnb  23119  restcls  23125  ordtbas2  23135  ordtopn1  23138  ordtopn2  23139  leordtval2  23156  iocpnfordt  23159  icomnfordt  23160  lecldbas  23163  pnrmopn  23287  cncmp  23336  fincmp  23337  cmpsublem  23343  cmpsub  23344  tgcmp  23345  uncmp  23347  cmpfi  23352  connsubclo  23368  2ndcomap  23402  dis2ndc  23404  cldllycmp  23439  dissnlocfin  23473  comppfsc  23476  ptpjopn  23556  txcmplem2  23586  qtopeu  23660  fbasrn  23828  elfm  23891  elfm3  23894  rnelfmlem  23896  rnelfm  23897  fmfnfmlem3  23900  fmfnfmlem4  23901  alexsubALTlem3  23993  ptcmplem2  23997  ptcmplem3  23998  ptcmplem5  24000  tsmsfbas  24072  trust  24173  restutopopn  24182  ustuqtop1  24185  ustuqtop2  24186  ustuqtop4  24188  ustuqtop5  24189  utopsnneiplem  24191  utopsnnei  24193  fmucnd  24235  neipcfilu  24239  mopnex  24463  metrest  24468  metustexhalf  24500  metustfbas  24501  cfilucfil  24503  restmetu  24514  metucn  24515  icoopnst  24892  iocopnst  24893  cnheibor  24910  minveclem2  25382  uniioombllem3  25542  itg1addlem4  25656  i1fmulc  25660  ply1lpir  26143  aannenlem2  26293  aalioulem2  26297  eflogeq  26567  cxpeq  26723  angpieqvd  26797  rlimcnp  26931  isppw2  27081  mpodvdsmulf1o  27160  dvdsmulf1o  27162  lgsquadlem1  27347  2sqlem2  27385  mul2sq  27386  2sqlem3  27387  2sqlem9  27394  2sqlem10  27395  ostth2  27604  ostth3  27605  bdayfo  27645  cutsfo  27901  addsproplem4  27968  addsproplem5  27969  addsproplem6  27970  addsfo  27979  subsfo  28061  elons2  28254  n0seo  28417  zseo  28418  midexlem  28764  midex  28809  ttgcontlem1  28957  axcontlem7  29043  upgrex  29165  erclwwlkref  30095  clwwlkfo  30125  erclwwlknref  30144  isgrpo  30572  grpoinvf  30607  minvecolem2  30950  shsel3  31390  pjhthlem2  31467  h1de2ctlem  31630  spansncol  31643  superpos  32429  cdj3lem2  32510  wrdsplex  33018  archiabllem1a  33273  archiabllem1b  33274  cmpcref  34007  ordtconnlem1  34081  gsumesum  34216  esumcst  34220  esumpcvgval  34235  sxbrsigalem2  34443  oms0  34454  omssubadd  34457  eulerpartlemt  34528  cvmsss2  35468  cvmfolem  35473  fobigcup  36092  opnregcld  36524  cldregopn  36525  onsucsuccmpi  36637  finixpnum  37806  poimirlem16  37837  poimirlem19  37840  itg2addnclem2  37873  isbnd2  37984  isbnd3  37985  totbndbnd  37990  heibor1lem  38010  heibor  38022  rngmgmbs4  38132  prnc  38268  prtlem11  39126  lsatlspsn2  39252  lsatlspsn  39253  lfl1dim  39381  lfl1dim2N  39382  lkrss2N  39429  glbconN  39637  atpointN  40003  ispsubcl2N  40207  dihglblem2aN  41553  dihglblem2N  41554  dihatexv  41598  dvh4dimat  41698  dochfl1  41736  lcfl8  41762  lcfrlem9  41810  mapdval2N  41890  mapdval4N  41892  mapdcv  41920  mapdspex  41928  hdmap14lem2a  42127  hdmap14lem6  42133  elrfi  42936  eldioph  43000  eldioph2b  43005  eldioph3  43008  eldioph4i  43054  rencldnfilem  43062  pellfund14  43140  rmxyelqirr  43152  filnm  43332  unxpwdom3  43337  lpirlnr  43359  hbt  43372  rngunsnply  43411  ofoafo  43598  naddcnffo  43606  oaun3lem1  43616  dvconstbi  44575  elrestd  45352  wessf1ornlem  45429  iccshift  45764  iooshift  45768  limcperiod  45874  sumnnodd  45876  dvnprodlem1  46190  itgperiod  46225  stirlinglem13  46330  sge0rnn0  46612  sge00  46620  fsumlesge0  46621  sge0tsms  46624  sge0cl  46625  sge0f1o  46626  sge0sup  46635  sge0resplit  46650  sge0xaddlem2  46678  sge0reuz  46691  sge0reuzb  46692  nnfoctbdjlem  46699  ovn0lem  46809  hoidmv1le  46838  hoidmvlelem1  46839  incsmflem  46985  decsmflem  47010  sigarcol  47108  7gbow  48018  0aryfvalel  48880  iscnrm3rlem2  49186