Theorem rspceeqv 3606

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2146  ∃wrex 3091

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092

This theorem is used by:  elrnmpt1s  5951  foco2  7108  fcofo  7295  onuninsuci  7842  fo1st  8012  fo2nd  8013  onnseq  8337  nneob  8648  ecelqs  8771  resixpfo  8940  elixpsn  8941  ixpsnf1o  8942  pwfilem  9284  fofinf1o  9296  elfir  9382  inelfi  9385  fiin  9389  djur  9921  cardalephex  10090  fin23lem38  10348  fin1a2lem11  10409  fin1a2lem13  10411  reclem3pr  11049  infm3lem  12188  ccats1pfxeqrex  14774  2cshwcshw  14886  cshwcshid  14888  cshwcsh2id  14889  shftlem  15129  shftfval  15131  isercoll2  15744  infcvgaux2i  15935  mertenslem1  15961  mertenslem2  15962  fprodser  16026  bezoutlem1  16619  pcprmpw  16965  1arithlem4  17008  vdwapun  17056  vdwlem1  17063  vdwlem2  17064  vdwlem6  17068  vdwlem8  17070  elrestr  17503  gsumwspan  18942  orbsta  19427  psgneldm2i  19619  odf1o2  19687  slwhash  19738  fislw  19739  lsmelvalm  19765  pj1id  19813  efgrelexlemb  19864  cyggeninv  19997  0cyg  20007  eldprdi  20134  lss1d  21134  lspsn  21173  pwssplit1  21230  lspsneq  21296  lspprat  21327  lpi0  21544  lpi1  21545  zringcyg  21669  znf1o  21751  cygznlem3  21769  frgpcyg  21773  islindf4  22038  clsval2  23257  restcld  23379  restcldi  23380  restopnb  23382  restcls  23388  ordtbas2  23398  ordtopn1  23401  ordtopn2  23402  leordtval2  23419  iocpnfordt  23422  icomnfordt  23423  lecldbas  23426  pnrmopn  23550  cncmp  23599  fincmp  23600  cmpsublem  23606  cmpsub  23607  tgcmp  23608  uncmp  23610  cmpfi  23615  connsubclo  23631  2ndcomap  23666  dis2ndc  23668  cldllycmp  23703  dissnlocfin  23737  comppfsc  23740  ptpjopn  23820  txcmplem2  23850  qtopeu  23924  fbasrn  24092  elfm  24155  elfm3  24158  rnelfmlem  24160  rnelfm  24161  fmfnfmlem3  24164  fmfnfmlem4  24165  alexsubALTlem3  24257  ptcmplem2  24261  ptcmplem3  24262  ptcmplem5  24264  tsmsfbas  24336  trust  24437  restutopopn  24446  ustuqtop1  24449  ustuqtop2  24450  ustuqtop4  24452  ustuqtop5  24453  utopsnneiplem  24455  utopsnnei  24457  fmucnd  24499  neipcfilu  24503  mopnex  24727  metrest  24732  metustexhalf  24764  metustfbas  24765  cfilucfil  24767  restmetu  24778  metucn  24779  icoopnst  25149  iocopnst  25150  cnheibor  25165  minveclem2  25636  uniioombllem3  25795  itg1addlem4  25909  i1fmulc  25913  ply1lpir  26390  aannenlem2  26543  aalioulem2  26547  eflogeq  26818  cxpeq  26973  angpieqvd  27047  rlimcnp  27181  isppw2  27330  mpodvdsmulf1o  27409  dvdsmulf1o  27411  lgsquadlem1  27595  2sqlem2  27633  mul2sq  27634  2sqlem3  27635  2sqlem9  27642  2sqlem10  27643  ostth2  27852  ostth3  27853  bdayfo  27892  cutsfo  28149  addsproplem4  28216  addsproplem5  28217  addsproplem6  28218  addsfo  28227  subsfo  28309  elons2  28502  n0seo  28665  zseo  28666  midexlem  29020  midex  29069  ttgcontlem1  29289  axcontlem7  29375  upgrex  29497  erclwwlkref  30438  clwwlkfo  30468  erclwwlknref  30487  isgrpo  30920  grpoinvf  30955  minvecolem2  31298  shsel3  31738  pjhthlem2  31815  h1de2ctlem  31978  spansncol  31991  superpos  32777  cdj3lem2  32858  wrdsplex  33326  archiabllem1a  33575  archiabllem1b  33576  cmpcref  34304  ordtconnlem1  34378  gsumesum  34513  esumcst  34517  esumpcvgval  34532  sxbrsigalem2  34741  oms0  34752  omssubadd  34755  eulerpartlemt  34826  rankfo  35563  cvmsss2  35803  cvmfolem  35808  fobigcup  36427  opnregcld  36898  cldregopn  36899  onsucsuccmpi  37011  finixpnum  38313  poimirlem16  38344  poimirlem19  38347  itg2addnclem2  38380  isbnd2  38492  isbnd3  38493  totbndbnd  38498  heibor1lem  38518  heibor  38530  rngmgmbs4  38640  prnc  38776  prtlem11  39698  lsatlspsn2  39824  lsatlspsn  39825  lfl1dim  39953  lfl1dim2N  39954  lkrss2N  40001  glbconN  40209  atpointN  40575  ispsubcl2N  40779  dihglblem2aN  42125  dihglblem2N  42126  dihatexv  42170  dvh4dimat  42270  dochfl1  42308  lcfl8  42334  lcfrlem9  42382  mapdval2N  42462  mapdval4N  42464  mapdcv  42492  mapdspex  42500  hdmap14lem2a  42699  hdmap14lem6  42705  elrfi  43483  eldioph  43547  eldioph2b  43552  eldioph3  43555  eldioph4i  43597  rencldnfilem  43605  pellfund14  43683  rmxyelqirr  43695  filnm  43875  unxpwdom3  43880  lpirlnr  43902  hbt  43915  rngunsnply  43954  ofoafo  44141  naddcnffo  44149  oaun3lem1  44159  dvconstbi  45102  elrestd  45884  wessf1ornlem  45961  iccshift  46292  iooshift  46296  limcperiod  46402  sumnnodd  46404  dvnprodlem1  46718  itgperiod  46753  stirlinglem13  46858  sge0rnn0  47140  sge00  47148  fsumlesge0  47149  sge0tsms  47152  sge0cl  47153  sge0f1o  47154  sge0sup  47163  sge0resplit  47178  sge0xaddlem2  47206  sge0reuz  47219  sge0reuzb  47220  nnfoctbdjlem  47227  ovn0lem  47337  hoidmv1le  47366  hoidmvlelem1  47367  incsmflem  47513  decsmflem  47538  sigarcol  47636  7gbow  48595  0aryfvalel  49471  iscnrm3rlem2  49776