Theorem rspceeqv 3588

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063

This theorem is referenced by:  elrnmpt1s  5909  foco2  7056  fcofo  7237  onuninsuci  7785  fo1st  7956  fo2nd  7957  onnseq  8278  nneob  8586  ecelqs  8708  resixpfo  8878  elixpsn  8879  ixpsnf1o  8880  pwfilem  9222  fofinf1o  9236  elfir  9322  inelfi  9325  fiin  9329  djur  9837  cardalephex  10006  fin23lem38  10265  fin1a2lem11  10326  fin1a2lem13  10328  reclem3pr  10966  infm3lem  12108  ccats1pfxeqrex  14671  2cshwcshw  14781  cshwcshid  14783  cshwcsh2id  14784  shftlem  15024  shftfval  15026  isercoll2  15625  infcvgaux2i  15817  mertenslem1  15843  mertenslem2  15844  fprodser  15908  bezoutlem1  16502  pcprmpw  16848  1arithlem4  16891  vdwapun  16939  vdwlem1  16946  vdwlem2  16947  vdwlem6  16951  vdwlem8  16953  elrestr  17385  gsumwspan  18808  orbsta  19282  psgneldm2i  19474  odf1o2  19542  slwhash  19593  fislw  19594  lsmelvalm  19620  pj1id  19668  efgrelexlemb  19719  cyggeninv  19852  0cyg  19862  eldprdi  19989  lss1d  20952  lspsn  20991  pwssplit1  21049  lspsneq  21115  lspprat  21146  lpi0  21319  lpi1  21320  zringcyg  21462  znf1o  21544  cygznlem3  21562  frgpcyg  21566  islindf4  21831  clsval2  23028  restcld  23150  restcldi  23151  restopnb  23153  restcls  23159  ordtbas2  23169  ordtopn1  23172  ordtopn2  23173  leordtval2  23190  iocpnfordt  23193  icomnfordt  23194  lecldbas  23197  pnrmopn  23321  cncmp  23370  fincmp  23371  cmpsublem  23377  cmpsub  23378  tgcmp  23379  uncmp  23381  cmpfi  23386  connsubclo  23402  2ndcomap  23436  dis2ndc  23438  cldllycmp  23473  dissnlocfin  23507  comppfsc  23510  ptpjopn  23590  txcmplem2  23620  qtopeu  23694  fbasrn  23862  elfm  23925  elfm3  23928  rnelfmlem  23930  rnelfm  23931  fmfnfmlem3  23934  fmfnfmlem4  23935  alexsubALTlem3  24027  ptcmplem2  24031  ptcmplem3  24032  ptcmplem5  24034  tsmsfbas  24106  trust  24207  restutopopn  24216  ustuqtop1  24219  ustuqtop2  24220  ustuqtop4  24222  ustuqtop5  24223  utopsnneiplem  24225  utopsnnei  24227  fmucnd  24269  neipcfilu  24273  mopnex  24497  metrest  24502  metustexhalf  24534  metustfbas  24535  cfilucfil  24537  restmetu  24548  metucn  24549  icoopnst  24919  iocopnst  24920  cnheibor  24935  minveclem2  25406  uniioombllem3  25565  itg1addlem4  25679  i1fmulc  25683  ply1lpir  26160  aannenlem2  26309  aalioulem2  26313  eflogeq  26582  cxpeq  26737  angpieqvd  26811  rlimcnp  26945  isppw2  27095  mpodvdsmulf1o  27174  dvdsmulf1o  27176  lgsquadlem1  27360  2sqlem2  27398  mul2sq  27399  2sqlem3  27400  2sqlem9  27407  2sqlem10  27408  ostth2  27617  ostth3  27618  bdayfo  27658  cutsfo  27914  addsproplem4  27981  addsproplem5  27982  addsproplem6  27983  addsfo  27992  subsfo  28074  elons2  28267  n0seo  28430  zseo  28431  midexlem  28777  midex  28822  ttgcontlem1  28970  axcontlem7  29056  upgrex  29178  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  33014  archiabllem1a  33270  archiabllem1b  33271  cmpcref  34013  ordtconnlem1  34087  gsumesum  34222  esumcst  34226  esumpcvgval  34241  sxbrsigalem2  34449  oms0  34460  omssubadd  34463  eulerpartlemt  34534  cvmsss2  35475  cvmfolem  35480  fobigcup  36099  opnregcld  36531  cldregopn  36532  onsucsuccmpi  36644  finixpnum  37943  poimirlem16  37974  poimirlem19  37977  itg2addnclem2  38010  isbnd2  38121  isbnd3  38122  totbndbnd  38127  heibor1lem  38147  heibor  38159  rngmgmbs4  38269  prnc  38405  prtlem11  39329  lsatlspsn2  39455  lsatlspsn  39456  lfl1dim  39584  lfl1dim2N  39585  lkrss2N  39632  glbconN  39840  atpointN  40206  ispsubcl2N  40410  dihglblem2aN  41756  dihglblem2N  41757  dihatexv  41801  dvh4dimat  41901  dochfl1  41939  lcfl8  41965  lcfrlem9  42013  mapdval2N  42093  mapdval4N  42095  mapdcv  42123  mapdspex  42131  hdmap14lem2a  42330  hdmap14lem6  42336  elrfi  43143  eldioph  43207  eldioph2b  43212  eldioph3  43215  eldioph4i  43261  rencldnfilem  43269  pellfund14  43347  rmxyelqirr  43359  filnm  43539  unxpwdom3  43544  lpirlnr  43566  hbt  43579  rngunsnply  43618  ofoafo  43805  naddcnffo  43813  oaun3lem1  43823  dvconstbi  44782  elrestd  45559  wessf1ornlem  45636  iccshift  45969  iooshift  45973  limcperiod  46079  sumnnodd  46081  dvnprodlem1  46395  itgperiod  46430  stirlinglem13  46535  sge0rnn0  46817  sge00  46825  fsumlesge0  46826  sge0tsms  46829  sge0cl  46830  sge0f1o  46831  sge0sup  46840  sge0resplit  46855  sge0xaddlem2  46883  sge0reuz  46896  sge0reuzb  46897  nnfoctbdjlem  46904  ovn0lem  47014  hoidmv1le  47043  hoidmvlelem1  47044  incsmflem  47190  decsmflem  47215  sigarcol  47313  7gbow  48263  0aryfvalel  49125  iscnrm3rlem2  49431