Theorem rspceeqv 3587

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 3564	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐸 = 𝐷) → ∃𝑥 ∈ 𝐵 𝐸 = 𝐶)

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062

This theorem is referenced by:  elrnmpt1s  5914  foco2  7061  fcofo  7243  onuninsuci  7791  fo1st  7962  fo2nd  7963  onnseq  8284  nneob  8592  ecelqs  8714  resixpfo  8884  elixpsn  8885  ixpsnf1o  8886  pwfilem  9228  fofinf1o  9242  elfir  9328  inelfi  9331  fiin  9335  djur  9843  cardalephex  10012  fin23lem38  10271  fin1a2lem11  10332  fin1a2lem13  10334  reclem3pr  10972  infm3lem  12114  ccats1pfxeqrex  14677  2cshwcshw  14787  cshwcshid  14789  cshwcsh2id  14790  shftlem  15030  shftfval  15032  isercoll2  15631  infcvgaux2i  15823  mertenslem1  15849  mertenslem2  15850  fprodser  15914  bezoutlem1  16508  pcprmpw  16854  1arithlem4  16897  vdwapun  16945  vdwlem1  16952  vdwlem2  16953  vdwlem6  16957  vdwlem8  16959  elrestr  17391  gsumwspan  18814  orbsta  19288  psgneldm2i  19480  odf1o2  19548  slwhash  19599  fislw  19600  lsmelvalm  19626  pj1id  19674  efgrelexlemb  19725  cyggeninv  19858  0cyg  19868  eldprdi  19995  lss1d  20958  lspsn  20997  pwssplit1  21054  lspsneq  21120  lspprat  21151  lpi0  21324  lpi1  21325  zringcyg  21449  znf1o  21531  cygznlem3  21549  frgpcyg  21553  islindf4  21818  clsval2  23015  restcld  23137  restcldi  23138  restopnb  23140  restcls  23146  ordtbas2  23156  ordtopn1  23159  ordtopn2  23160  leordtval2  23177  iocpnfordt  23180  icomnfordt  23181  lecldbas  23184  pnrmopn  23308  cncmp  23357  fincmp  23358  cmpsublem  23364  cmpsub  23365  tgcmp  23366  uncmp  23368  cmpfi  23373  connsubclo  23389  2ndcomap  23423  dis2ndc  23425  cldllycmp  23460  dissnlocfin  23494  comppfsc  23497  ptpjopn  23577  txcmplem2  23607  qtopeu  23681  fbasrn  23849  elfm  23912  elfm3  23915  rnelfmlem  23917  rnelfm  23918  fmfnfmlem3  23921  fmfnfmlem4  23922  alexsubALTlem3  24014  ptcmplem2  24018  ptcmplem3  24019  ptcmplem5  24021  tsmsfbas  24093  trust  24194  restutopopn  24203  ustuqtop1  24206  ustuqtop2  24207  ustuqtop4  24209  ustuqtop5  24210  utopsnneiplem  24212  utopsnnei  24214  fmucnd  24256  neipcfilu  24260  mopnex  24484  metrest  24489  metustexhalf  24521  metustfbas  24522  cfilucfil  24524  restmetu  24535  metucn  24536  icoopnst  24906  iocopnst  24907  cnheibor  24922  minveclem2  25393  uniioombllem3  25552  itg1addlem4  25666  i1fmulc  25670  ply1lpir  26147  aannenlem2  26295  aalioulem2  26299  eflogeq  26566  cxpeq  26721  angpieqvd  26795  rlimcnp  26929  isppw2  27078  mpodvdsmulf1o  27157  dvdsmulf1o  27159  lgsquadlem1  27343  2sqlem2  27381  mul2sq  27382  2sqlem3  27383  2sqlem9  27390  2sqlem10  27391  ostth2  27600  ostth3  27601  bdayfo  27641  cutsfo  27897  addsproplem4  27964  addsproplem5  27965  addsproplem6  27966  addsfo  27975  subsfo  28057  elons2  28250  n0seo  28413  zseo  28414  midexlem  28760  midex  28805  ttgcontlem1  28953  axcontlem7  29039  upgrex  29161  erclwwlkref  30090  clwwlkfo  30120  erclwwlknref  30139  isgrpo  30568  grpoinvf  30603  minvecolem2  30946  shsel3  31386  pjhthlem2  31463  h1de2ctlem  31626  spansncol  31639  superpos  32425  cdj3lem2  32506  wrdsplex  32996  archiabllem1a  33252  archiabllem1b  33253  cmpcref  33994  ordtconnlem1  34068  gsumesum  34203  esumcst  34207  esumpcvgval  34222  sxbrsigalem2  34430  oms0  34441  omssubadd  34444  eulerpartlemt  34515  cvmsss2  35456  cvmfolem  35461  fobigcup  36080  opnregcld  36512  cldregopn  36513  onsucsuccmpi  36625  finixpnum  37926  poimirlem16  37957  poimirlem19  37960  itg2addnclem2  37993  isbnd2  38104  isbnd3  38105  totbndbnd  38110  heibor1lem  38130  heibor  38142  rngmgmbs4  38252  prnc  38388  prtlem11  39312  lsatlspsn2  39438  lsatlspsn  39439  lfl1dim  39567  lfl1dim2N  39568  lkrss2N  39615  glbconN  39823  atpointN  40189  ispsubcl2N  40393  dihglblem2aN  41739  dihglblem2N  41740  dihatexv  41784  dvh4dimat  41884  dochfl1  41922  lcfl8  41948  lcfrlem9  41996  mapdval2N  42076  mapdval4N  42078  mapdcv  42106  mapdspex  42114  hdmap14lem2a  42313  hdmap14lem6  42319  elrfi  43126  eldioph  43190  eldioph2b  43195  eldioph3  43198  eldioph4i  43240  rencldnfilem  43248  pellfund14  43326  rmxyelqirr  43338  filnm  43518  unxpwdom3  43523  lpirlnr  43545  hbt  43558  rngunsnply  43597  ofoafo  43784  naddcnffo  43792  oaun3lem1  43802  dvconstbi  44761  elrestd  45538  wessf1ornlem  45615  iccshift  45948  iooshift  45952  limcperiod  46058  sumnnodd  46060  dvnprodlem1  46374  itgperiod  46409  stirlinglem13  46514  sge0rnn0  46796  sge00  46804  fsumlesge0  46805  sge0tsms  46808  sge0cl  46809  sge0f1o  46810  sge0sup  46819  sge0resplit  46834  sge0xaddlem2  46862  sge0reuz  46875  sge0reuzb  46876  nnfoctbdjlem  46883  ovn0lem  46993  hoidmv1le  47022  hoidmvlelem1  47023  incsmflem  47169  decsmflem  47194  sigarcol  47292  7gbow  48248  0aryfvalel  49110  iscnrm3rlem2  49416