Theorem rspceeqv 3599

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

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

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 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088

This theorem is used by:  elrnmpt1s  5941  foco2  7109  fcofo  7296  onuninsuci  7851  fo1st  8021  fo2nd  8022  onnseq  8352  nneob  8665  ecelqs  8788  resixpfo  8964  elixpsn  8965  ixpsnf1o  8966  pwfilem  9309  fofinf1o  9321  elfir  9407  inelfi  9410  fiin  9414  djur  10000  cardalephex  10169  fin23lem38  10427  fin1a2lem11  10488  fin1a2lem13  10490  reclem3pr  11134  infm3lem  12275  ccats1pfxeqrex  14864  2cshwcshw  14976  cshwcshid  14978  cshwcsh2id  14979  shftlem  15221  shftfval  15223  isercoll2  15836  infcvgaux2i  16027  mertenslem1  16053  mertenslem2  16054  fprodser  16116  bezoutlem1  16712  pcprmpw  17061  1arithlem4  17104  vdwapun  17152  vdwlem1  17159  vdwlem2  17160  vdwlem6  17164  vdwlem8  17166  elrestr  17599  gsumwspan  19042  orbsta  19527  psgneldm2i  19719  odf1o2  19787  slwhash  19838  fislw  19839  lsmelvalm  19865  pj1id  19913  efgrelexlemb  19964  cyggeninv  20097  0cyg  20107  eldprdi  20234  lss1d  21238  lspsn  21277  pwssplit1  21334  lspsneq  21400  lspprat  21431  lpi0  21650  lpi1  21651  zringcyg  21775  znf1o  21857  cygznlem3  21875  frgpcyg  21879  islindf4  22144  clsval2  23368  restcld  23490  restcldi  23491  restopnb  23493  restcls  23499  ordtbas2  23509  ordtopn1  23512  ordtopn2  23513  leordtval2  23530  iocpnfordt  23533  icomnfordt  23534  lecldbas  23537  pnrmopn  23661  cncmp  23710  fincmp  23711  cmpsublem  23717  cmpsub  23718  tgcmp  23719  uncmp  23721  cmpfi  23726  connsubclo  23742  2ndcomap  23777  dis2ndc  23779  cldllycmp  23814  dissnlocfin  23848  comppfsc  23851  ptpjopn  23931  txcmplem2  23961  qtopeu  24035  fbasrn  24203  elfm  24266  elfm3  24269  rnelfmlem  24271  rnelfm  24272  fmfnfmlem3  24275  fmfnfmlem4  24276  alexsubALTlem3  24368  ptcmplem2  24372  ptcmplem3  24373  ptcmplem5  24375  tsmsfbas  24447  trust  24548  restutopopn  24557  ustuqtop1  24560  ustuqtop2  24561  ustuqtop4  24563  ustuqtop5  24564  utopsnneiplem  24566  utopsnnei  24568  fmucnd  24610  neipcfilu  24614  mopnex  24838  metrest  24843  metustexhalf  24875  metustfbas  24876  cfilucfil  24878  restmetu  24889  metucn  24890  icoopnst  25260  iocopnst  25261  cnheibor  25276  minveclem2  25747  uniioombllem3  25906  itg1addlem4  26020  i1fmulc  26024  ply1lpir  26500  aannenlem2  26656  aalioulem2  26660  eflogeq  26930  cxpeq  27085  angpieqvd  27159  rlimcnp  27293  isppw2  27442  mpodvdsmulf1o  27521  dvdsmulf1o  27523  lgsquadlem1  27707  2sqlem2  27745  mul2sq  27746  2sqlem3  27747  2sqlem9  27754  2sqlem10  27755  ostth2  27964  ostth3  27965  bdayfo  28034  cutsfo  28291  addsproplem4  28358  addsproplem5  28359  addsproplem6  28360  addsfo  28369  subsfo  28451  elons2  28644  n0seo  28807  zseo  28808  midexlem  29164  midex  29213  ttgcontlem1  29462  axcontlem7  29548  upgrex  29670  erclwwlkref  30611  clwwlkfo  30641  erclwwlknref  30660  isgrpo  31099  grpoinvf  31134  minvecolem2  31477  shsel3  31917  pjhthlem2  31994  h1de2ctlem  32157  spansncol  32170  superpos  32956  cdj3lem2  33037  wrdsplex  33503  archiabllem1a  33752  archiabllem1b  33753  cmpcref  34482  ordtconnlem1  34556  gsumesum  34691  esumcst  34695  esumpcvgval  34710  sxbrsigalem2  34918  oms0  34929  omssubadd  34932  eulerpartlemt  35003  rankfo  35735  cvmsss2  36039  cvmfolem  36044  fobigcup  36662  opnregcld  37118  cldregopn  37119  onsucsuccmpi  37231  finixpnum  38528  poimirlem16  38554  poimirlem19  38557  itg2addnclem2  38590  isbnd2  38717  isbnd3  38718  totbndbnd  38723  heibor1lem  38743  heibor  38755  rngmgmbs4  38865  prnc  39001  prtlem11  39923  lsatlspsn2  40049  lsatlspsn  40050  lfl1dim  40178  lfl1dim2N  40179  lkrss2N  40226  glbconN  40434  atpointN  40800  ispsubcl2N  41004  dihglblem2aN  42350  dihglblem2N  42351  dihatexv  42395  dvh4dimat  42495  dochfl1  42533  lcfl8  42559  lcfrlem9  42607  mapdval2N  42687  mapdval4N  42689  mapdcv  42717  mapdspex  42725  hdmap14lem2a  42924  hdmap14lem6  42930  elrfi  43704  eldioph  43768  eldioph2b  43773  eldioph3  43776  eldioph4i  43818  rencldnfilem  43826  pellfund14  43904  rmxyelqirr  43916  filnm  44091  unxpwdom3  44096  lpirlnr  44118  hbt  44131  rngunsnply  44170  ofoafo  44357  naddcnffo  44365  oaun3lem1  44375  dvconstbi  45317  elrestd  46122  wessf1ornlem  46199  iccshift  46529  iooshift  46533  limcperiod  46639  sumnnodd  46641  dvnprodlem1  46955  itgperiod  46990  stirlinglem13  47095  sge0rnn0  47377  sge00  47385  fsumlesge0  47386  sge0tsms  47389  sge0cl  47390  sge0f1o  47391  sge0sup  47400  sge0resplit  47415  sge0xaddlem2  47443  sge0reuz  47456  sge0reuzb  47457  nnfoctbdjlem  47464  ovn0lem  47574  hoidmv1le  47603  hoidmvlelem1  47604  incsmflem  47750  decsmflem  47775  sigarcol  47873  7gbow  48869  0aryfvalel  49745  iscnrm3rlem2  50048