Theorem rspceeqv 3601

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 3578	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  5916  foco2  7063  fcofo  7244  onuninsuci  7792  fo1st  7963  fo2nd  7964  onnseq  8286  nneob  8594  ecelqs  8716  resixpfo  8886  elixpsn  8887  ixpsnf1o  8888  pwfilem  9230  fofinf1o  9244  elfir  9330  inelfi  9333  fiin  9337  djur  9843  cardalephex  10012  fin23lem38  10271  fin1a2lem11  10332  fin1a2lem13  10334  reclem3pr  10972  infm3lem  12112  ccats1pfxeqrex  14650  2cshwcshw  14760  cshwcshid  14762  cshwcsh2id  14763  shftlem  15003  shftfval  15005  isercoll2  15604  infcvgaux2i  15793  mertenslem1  15819  mertenslem2  15820  fprodser  15884  bezoutlem1  16478  pcprmpw  16823  1arithlem4  16866  vdwapun  16914  vdwlem1  16921  vdwlem2  16922  vdwlem6  16926  vdwlem8  16928  elrestr  17360  gsumwspan  18783  orbsta  19254  psgneldm2i  19446  odf1o2  19514  slwhash  19565  fislw  19566  lsmelvalm  19592  pj1id  19640  efgrelexlemb  19691  cyggeninv  19824  0cyg  19834  eldprdi  19961  lss1d  20926  lspsn  20965  pwssplit1  21023  lspsneq  21089  lspprat  21120  lpi0  21293  lpi1  21294  zringcyg  21436  znf1o  21518  cygznlem3  21536  frgpcyg  21540  islindf4  21805  clsval2  23006  restcld  23128  restcldi  23129  restopnb  23131  restcls  23137  ordtbas2  23147  ordtopn1  23150  ordtopn2  23151  leordtval2  23168  iocpnfordt  23171  icomnfordt  23172  lecldbas  23175  pnrmopn  23299  cncmp  23348  fincmp  23349  cmpsublem  23355  cmpsub  23356  tgcmp  23357  uncmp  23359  cmpfi  23364  connsubclo  23380  2ndcomap  23414  dis2ndc  23416  cldllycmp  23451  dissnlocfin  23485  comppfsc  23488  ptpjopn  23568  txcmplem2  23598  qtopeu  23672  fbasrn  23840  elfm  23903  elfm3  23906  rnelfmlem  23908  rnelfm  23909  fmfnfmlem3  23912  fmfnfmlem4  23913  alexsubALTlem3  24005  ptcmplem2  24009  ptcmplem3  24010  ptcmplem5  24012  tsmsfbas  24084  trust  24185  restutopopn  24194  ustuqtop1  24197  ustuqtop2  24198  ustuqtop4  24200  ustuqtop5  24201  utopsnneiplem  24203  utopsnnei  24205  fmucnd  24247  neipcfilu  24251  mopnex  24475  metrest  24480  metustexhalf  24512  metustfbas  24513  cfilucfil  24515  restmetu  24526  metucn  24527  icoopnst  24904  iocopnst  24905  cnheibor  24922  minveclem2  25394  uniioombllem3  25554  itg1addlem4  25668  i1fmulc  25672  ply1lpir  26155  aannenlem2  26305  aalioulem2  26309  eflogeq  26579  cxpeq  26735  angpieqvd  26809  rlimcnp  26943  isppw2  27093  mpodvdsmulf1o  27172  dvdsmulf1o  27174  lgsquadlem1  27359  2sqlem2  27397  mul2sq  27398  2sqlem3  27399  2sqlem9  27406  2sqlem10  27407  ostth2  27616  ostth3  27617  bdayfo  27657  cutsfo  27913  addsproplem4  27980  addsproplem5  27981  addsproplem6  27982  addsfo  27991  subsfo  28073  elons2  28266  n0seo  28429  zseo  28430  midexlem  28776  midex  28821  ttgcontlem1  28969  axcontlem7  29055  upgrex  29177  erclwwlkref  30107  clwwlkfo  30137  erclwwlknref  30156  isgrpo  30585  grpoinvf  30620  minvecolem2  30963  shsel3  31403  pjhthlem2  31480  h1de2ctlem  31643  spansncol  31656  superpos  32442  cdj3lem2  32523  wrdsplex  33029  archiabllem1a  33285  archiabllem1b  33286  cmpcref  34028  ordtconnlem1  34102  gsumesum  34237  esumcst  34241  esumpcvgval  34256  sxbrsigalem2  34464  oms0  34475  omssubadd  34478  eulerpartlemt  34549  cvmsss2  35490  cvmfolem  35495  fobigcup  36114  opnregcld  36546  cldregopn  36547  onsucsuccmpi  36659  finixpnum  37856  poimirlem16  37887  poimirlem19  37890  itg2addnclem2  37923  isbnd2  38034  isbnd3  38035  totbndbnd  38040  heibor1lem  38060  heibor  38072  rngmgmbs4  38182  prnc  38318  prtlem11  39242  lsatlspsn2  39368  lsatlspsn  39369  lfl1dim  39497  lfl1dim2N  39498  lkrss2N  39545  glbconN  39753  atpointN  40119  ispsubcl2N  40323  dihglblem2aN  41669  dihglblem2N  41670  dihatexv  41714  dvh4dimat  41814  dochfl1  41852  lcfl8  41878  lcfrlem9  41926  mapdval2N  42006  mapdval4N  42008  mapdcv  42036  mapdspex  42044  hdmap14lem2a  42243  hdmap14lem6  42249  elrfi  43051  eldioph  43115  eldioph2b  43120  eldioph3  43123  eldioph4i  43169  rencldnfilem  43177  pellfund14  43255  rmxyelqirr  43267  filnm  43447  unxpwdom3  43452  lpirlnr  43474  hbt  43487  rngunsnply  43526  ofoafo  43713  naddcnffo  43721  oaun3lem1  43731  dvconstbi  44690  elrestd  45467  wessf1ornlem  45544  iccshift  45878  iooshift  45882  limcperiod  45988  sumnnodd  45990  dvnprodlem1  46304  itgperiod  46339  stirlinglem13  46444  sge0rnn0  46726  sge00  46734  fsumlesge0  46735  sge0tsms  46738  sge0cl  46739  sge0f1o  46740  sge0sup  46749  sge0resplit  46764  sge0xaddlem2  46792  sge0reuz  46805  sge0reuzb  46806  nnfoctbdjlem  46813  ovn0lem  46923  hoidmv1le  46952  hoidmvlelem1  46953  incsmflem  47099  decsmflem  47124  sigarcol  47222  7gbow  48132  0aryfvalel  48994  iscnrm3rlem2  49300