Theorem rspceeqv 3583

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119  ∃wrex 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064

This theorem is referenced by:  elrnmpt1s  5901  foco2  7050  fcofo  7232  onuninsuci  7780  fo1st  7951  fo2nd  7952  onnseq  8274  nneob  8582  ecelqs  8704  resixpfo  8874  elixpsn  8875  ixpsnf1o  8876  pwfilem  9218  fofinf1o  9232  elfir  9318  inelfi  9321  fiin  9325  djur  9834  cardalephex  10003  fin23lem38  10262  fin1a2lem11  10323  fin1a2lem13  10325  reclem3pr  10963  infm3lem  12105  ccats1pfxeqrex  14668  2cshwcshw  14778  cshwcshid  14780  cshwcsh2id  14781  shftlem  15021  shftfval  15023  isercoll2  15622  infcvgaux2i  15814  mertenslem1  15840  mertenslem2  15841  fprodser  15905  bezoutlem1  16499  pcprmpw  16845  1arithlem4  16888  vdwapun  16936  vdwlem1  16943  vdwlem2  16944  vdwlem6  16948  vdwlem8  16950  elrestr  17382  gsumwspan  18805  orbsta  19279  psgneldm2i  19471  odf1o2  19539  slwhash  19590  fislw  19591  lsmelvalm  19617  pj1id  19665  efgrelexlemb  19716  cyggeninv  19849  0cyg  19859  eldprdi  19986  lss1d  20953  lspsn  20992  pwssplit1  21049  lspsneq  21115  lspprat  21146  lpi0  21319  lpi1  21320  zringcyg  21444  znf1o  21526  cygznlem3  21544  frgpcyg  21548  islindf4  21813  clsval2  23033  restcld  23155  restcldi  23156  restopnb  23158  restcls  23164  ordtbas2  23174  ordtopn1  23177  ordtopn2  23178  leordtval2  23195  iocpnfordt  23198  icomnfordt  23199  lecldbas  23202  pnrmopn  23326  cncmp  23375  fincmp  23376  cmpsublem  23382  cmpsub  23383  tgcmp  23384  uncmp  23386  cmpfi  23391  connsubclo  23407  2ndcomap  23441  dis2ndc  23443  cldllycmp  23478  dissnlocfin  23512  comppfsc  23515  ptpjopn  23595  txcmplem2  23625  qtopeu  23699  fbasrn  23867  elfm  23930  elfm3  23933  rnelfmlem  23935  rnelfm  23936  fmfnfmlem3  23939  fmfnfmlem4  23940  alexsubALTlem3  24032  ptcmplem2  24036  ptcmplem3  24037  ptcmplem5  24039  tsmsfbas  24111  trust  24212  restutopopn  24221  ustuqtop1  24224  ustuqtop2  24225  ustuqtop4  24227  ustuqtop5  24228  utopsnneiplem  24230  utopsnnei  24232  fmucnd  24274  neipcfilu  24278  mopnex  24502  metrest  24507  metustexhalf  24539  metustfbas  24540  cfilucfil  24542  restmetu  24553  metucn  24554  icoopnst  24924  iocopnst  24925  cnheibor  24940  minveclem2  25411  uniioombllem3  25570  itg1addlem4  25684  i1fmulc  25688  ply1lpir  26165  aannenlem2  26313  aalioulem2  26317  eflogeq  26584  cxpeq  26739  angpieqvd  26813  rlimcnp  26947  isppw2  27096  mpodvdsmulf1o  27175  dvdsmulf1o  27177  lgsquadlem1  27361  2sqlem2  27399  mul2sq  27400  2sqlem3  27401  2sqlem9  27408  2sqlem10  27409  ostth2  27618  ostth3  27619  bdayfo  27659  cutsfo  27915  addsproplem4  27982  addsproplem5  27983  addsproplem6  27984  addsfo  27993  subsfo  28075  elons2  28268  n0seo  28431  zseo  28432  midexlem  28778  midex  28823  ttgcontlem1  28971  axcontlem7  29057  upgrex  29179  erclwwlkref  30108  clwwlkfo  30138  erclwwlknref  30157  isgrpo  30586  grpoinvf  30621  minvecolem2  30964  shsel3  31404  pjhthlem2  31481  h1de2ctlem  31644  spansncol  31657  superpos  32443  cdj3lem2  32524  wrdsplex  33015  archiabllem1a  33272  archiabllem1b  33273  cmpcref  34034  ordtconnlem1  34108  gsumesum  34243  esumcst  34247  esumpcvgval  34262  sxbrsigalem2  34470  oms0  34481  omssubadd  34484  eulerpartlemt  34555  cvmsss2  35502  cvmfolem  35507  fobigcup  36126  opnregcld  36558  cldregopn  36559  onsucsuccmpi  36671  finixpnum  37972  poimirlem16  38003  poimirlem19  38006  itg2addnclem2  38039  isbnd2  38150  isbnd3  38151  totbndbnd  38156  heibor1lem  38176  heibor  38188  rngmgmbs4  38298  prnc  38434  prtlem11  39358  lsatlspsn2  39484  lsatlspsn  39485  lfl1dim  39613  lfl1dim2N  39614  lkrss2N  39661  glbconN  39869  atpointN  40235  ispsubcl2N  40439  dihglblem2aN  41785  dihglblem2N  41786  dihatexv  41830  dvh4dimat  41930  dochfl1  41968  lcfl8  41994  lcfrlem9  42042  mapdval2N  42122  mapdval4N  42124  mapdcv  42152  mapdspex  42160  hdmap14lem2a  42359  hdmap14lem6  42365  elrfi  43143  eldioph  43207  eldioph2b  43212  eldioph3  43215  eldioph4i  43257  rencldnfilem  43265  pellfund14  43343  rmxyelqirr  43355  filnm  43535  unxpwdom3  43540  lpirlnr  43562  hbt  43575  rngunsnply  43614  ofoafo  43801  naddcnffo  43809  oaun3lem1  43819  dvconstbi  44778  elrestd  45555  wessf1ornlem  45632  iccshift  45963  iooshift  45967  limcperiod  46073  sumnnodd  46075  dvnprodlem1  46389  itgperiod  46424  stirlinglem13  46529  sge0rnn0  46811  sge00  46819  fsumlesge0  46820  sge0tsms  46823  sge0cl  46824  sge0f1o  46825  sge0sup  46834  sge0resplit  46849  sge0xaddlem2  46877  sge0reuz  46890  sge0reuzb  46891  nnfoctbdjlem  46898  ovn0lem  47008  hoidmv1le  47037  hoidmvlelem1  47038  incsmflem  47184  decsmflem  47209  sigarcol  47307  7gbow  48263  0aryfvalel  49125  iscnrm3rlem2  49431