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  5906  foco2  7053  fcofo  7234  onuninsuci  7782  fo1st  7953  fo2nd  7954  onnseq  8275  nneob  8583  ecelqs  8705  resixpfo  8875  elixpsn  8876  ixpsnf1o  8877  pwfilem  9219  fofinf1o  9233  elfir  9319  inelfi  9322  fiin  9326  djur  9832  cardalephex  10001  fin23lem38  10260  fin1a2lem11  10321  fin1a2lem13  10323  reclem3pr  10961  infm3lem  12101  ccats1pfxeqrex  14639  2cshwcshw  14749  cshwcshid  14751  cshwcsh2id  14752  shftlem  14992  shftfval  14994  isercoll2  15593  infcvgaux2i  15782  mertenslem1  15808  mertenslem2  15809  fprodser  15873  bezoutlem1  16467  pcprmpw  16812  1arithlem4  16855  vdwapun  16903  vdwlem1  16910  vdwlem2  16911  vdwlem6  16915  vdwlem8  16917  elrestr  17349  gsumwspan  18772  orbsta  19246  psgneldm2i  19438  odf1o2  19506  slwhash  19557  fislw  19558  lsmelvalm  19584  pj1id  19632  efgrelexlemb  19683  cyggeninv  19816  0cyg  19826  eldprdi  19953  lss1d  20916  lspsn  20955  pwssplit1  21013  lspsneq  21079  lspprat  21110  lpi0  21283  lpi1  21284  zringcyg  21426  znf1o  21508  cygznlem3  21526  frgpcyg  21530  islindf4  21795  clsval2  22993  restcld  23115  restcldi  23116  restopnb  23118  restcls  23124  ordtbas2  23134  ordtopn1  23137  ordtopn2  23138  leordtval2  23155  iocpnfordt  23158  icomnfordt  23159  lecldbas  23162  pnrmopn  23286  cncmp  23335  fincmp  23336  cmpsublem  23342  cmpsub  23343  tgcmp  23344  uncmp  23346  cmpfi  23351  connsubclo  23367  2ndcomap  23401  dis2ndc  23403  cldllycmp  23438  dissnlocfin  23472  comppfsc  23475  ptpjopn  23555  txcmplem2  23585  qtopeu  23659  fbasrn  23827  elfm  23890  elfm3  23893  rnelfmlem  23895  rnelfm  23896  fmfnfmlem3  23899  fmfnfmlem4  23900  alexsubALTlem3  23992  ptcmplem2  23996  ptcmplem3  23997  ptcmplem5  23999  tsmsfbas  24071  trust  24172  restutopopn  24181  ustuqtop1  24184  ustuqtop2  24185  ustuqtop4  24187  ustuqtop5  24188  utopsnneiplem  24190  utopsnnei  24192  fmucnd  24234  neipcfilu  24238  mopnex  24462  metrest  24467  metustexhalf  24499  metustfbas  24500  cfilucfil  24502  restmetu  24513  metucn  24514  icoopnst  24884  iocopnst  24885  cnheibor  24900  minveclem2  25371  uniioombllem3  25530  itg1addlem4  25644  i1fmulc  25648  ply1lpir  26128  aannenlem2  26277  aalioulem2  26281  eflogeq  26551  cxpeq  26707  angpieqvd  26781  rlimcnp  26915  isppw2  27065  mpodvdsmulf1o  27144  dvdsmulf1o  27146  lgsquadlem1  27331  2sqlem2  27369  mul2sq  27370  2sqlem3  27371  2sqlem9  27378  2sqlem10  27379  ostth2  27588  ostth3  27589  bdayfo  27629  cutsfo  27885  addsproplem4  27952  addsproplem5  27953  addsproplem6  27954  addsfo  27963  subsfo  28045  elons2  28238  n0seo  28401  zseo  28402  midexlem  28748  midex  28793  ttgcontlem1  28941  axcontlem7  29027  upgrex  29149  erclwwlkref  30079  clwwlkfo  30109  erclwwlknref  30128  isgrpo  30557  grpoinvf  30592  minvecolem2  30935  shsel3  31375  pjhthlem2  31452  h1de2ctlem  31615  spansncol  31628  superpos  32414  cdj3lem2  32495  wrdsplex  33001  archiabllem1a  33257  archiabllem1b  33258  cmpcref  34000  ordtconnlem1  34074  gsumesum  34209  esumcst  34213  esumpcvgval  34228  sxbrsigalem2  34436  oms0  34447  omssubadd  34450  eulerpartlemt  34521  cvmsss2  35462  cvmfolem  35467  fobigcup  36086  opnregcld  36518  cldregopn  36519  onsucsuccmpi  36631  finixpnum  37917  poimirlem16  37948  poimirlem19  37951  itg2addnclem2  37984  isbnd2  38095  isbnd3  38096  totbndbnd  38101  heibor1lem  38121  heibor  38133  rngmgmbs4  38243  prnc  38379  prtlem11  39303  lsatlspsn2  39429  lsatlspsn  39430  lfl1dim  39558  lfl1dim2N  39559  lkrss2N  39606  glbconN  39814  atpointN  40180  ispsubcl2N  40384  dihglblem2aN  41730  dihglblem2N  41731  dihatexv  41775  dvh4dimat  41875  dochfl1  41913  lcfl8  41939  lcfrlem9  41987  mapdval2N  42067  mapdval4N  42069  mapdcv  42097  mapdspex  42105  hdmap14lem2a  42304  hdmap14lem6  42310  elrfi  43125  eldioph  43189  eldioph2b  43194  eldioph3  43197  eldioph4i  43243  rencldnfilem  43251  pellfund14  43329  rmxyelqirr  43341  filnm  43521  unxpwdom3  43526  lpirlnr  43548  hbt  43561  rngunsnply  43600  ofoafo  43787  naddcnffo  43795  oaun3lem1  43805  dvconstbi  44764  elrestd  45541  wessf1ornlem  45618  iccshift  45952  iooshift  45956  limcperiod  46062  sumnnodd  46064  dvnprodlem1  46378  itgperiod  46413  stirlinglem13  46518  sge0rnn0  46800  sge00  46808  fsumlesge0  46809  sge0tsms  46812  sge0cl  46813  sge0f1o  46814  sge0sup  46823  sge0resplit  46838  sge0xaddlem2  46866  sge0reuz  46879  sge0reuzb  46880  nnfoctbdjlem  46887  ovn0lem  46997  hoidmv1le  47026  hoidmvlelem1  47027  incsmflem  47173  decsmflem  47198  sigarcol  47296  7gbow  48206  0aryfvalel  49068  iscnrm3rlem2  49374