Theorem rspceeqv 3600

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054

This theorem is referenced by:  elrnmpt1s  5901  foco2  7043  fcofo  7225  onuninsuci  7773  fo1st  7944  fo2nd  7945  onnseq  8267  nneob  8574  ecelqs  8695  resixpfo  8863  elixpsn  8864  ixpsnf1o  8865  pwfilem  9207  fofinf1o  9222  elfir  9305  inelfi  9308  fiin  9312  djur  9815  cardalephex  9984  fin23lem38  10243  fin1a2lem11  10304  fin1a2lem13  10306  reclem3pr  10943  infm3lem  12083  ccats1pfxeqrex  14621  2cshwcshw  14732  cshwcshid  14734  cshwcsh2id  14735  shftlem  14975  shftfval  14977  isercoll2  15576  infcvgaux2i  15765  mertenslem1  15791  mertenslem2  15792  fprodser  15856  bezoutlem1  16450  pcprmpw  16795  1arithlem4  16838  vdwapun  16886  vdwlem1  16893  vdwlem2  16894  vdwlem6  16898  vdwlem8  16900  elrestr  17332  gsumwspan  18720  orbsta  19192  psgneldm2i  19384  odf1o2  19452  slwhash  19503  fislw  19504  lsmelvalm  19530  pj1id  19578  efgrelexlemb  19629  cyggeninv  19762  0cyg  19772  eldprdi  19899  lss1d  20866  lspsn  20905  pwssplit1  20963  lspsneq  21029  lspprat  21060  lpi0  21233  lpi1  21234  zringcyg  21376  znf1o  21458  cygznlem3  21476  frgpcyg  21480  islindf4  21745  clsval2  22935  restcld  23057  restcldi  23058  restopnb  23060  restcls  23066  ordtbas2  23076  ordtopn1  23079  ordtopn2  23080  leordtval2  23097  iocpnfordt  23100  icomnfordt  23101  lecldbas  23104  pnrmopn  23228  cncmp  23277  fincmp  23278  cmpsublem  23284  cmpsub  23285  tgcmp  23286  uncmp  23288  cmpfi  23293  connsubclo  23309  2ndcomap  23343  dis2ndc  23345  cldllycmp  23380  dissnlocfin  23414  comppfsc  23417  ptpjopn  23497  txcmplem2  23527  qtopeu  23601  fbasrn  23769  elfm  23832  elfm3  23835  rnelfmlem  23837  rnelfm  23838  fmfnfmlem3  23841  fmfnfmlem4  23842  alexsubALTlem3  23934  ptcmplem2  23938  ptcmplem3  23939  ptcmplem5  23941  tsmsfbas  24013  trust  24115  restutopopn  24124  ustuqtop1  24127  ustuqtop2  24128  ustuqtop4  24130  ustuqtop5  24131  utopsnneiplem  24133  utopsnnei  24135  fmucnd  24177  neipcfilu  24181  mopnex  24405  metrest  24410  metustexhalf  24442  metustfbas  24443  cfilucfil  24445  restmetu  24456  metucn  24457  icoopnst  24834  iocopnst  24835  cnheibor  24852  minveclem2  25324  uniioombllem3  25484  itg1addlem4  25598  i1fmulc  25602  ply1lpir  26085  aannenlem2  26235  aalioulem2  26239  eflogeq  26509  cxpeq  26665  angpieqvd  26739  rlimcnp  26873  isppw2  27023  mpodvdsmulf1o  27102  dvdsmulf1o  27104  lgsquadlem1  27289  2sqlem2  27327  mul2sq  27328  2sqlem3  27329  2sqlem9  27336  2sqlem10  27337  ostth2  27546  ostth3  27547  bdayfo  27587  scutfo  27819  addsproplem4  27884  addsproplem5  27885  addsproplem6  27886  addsfo  27895  subsfo  27974  elons2  28164  n0seo  28313  zseo  28314  midexlem  28637  midex  28682  ttgcontlem1  28830  axcontlem7  28915  upgrex  29037  erclwwlkref  29964  clwwlkfo  29994  erclwwlknref  30013  isgrpo  30441  grpoinvf  30476  minvecolem2  30819  shsel3  31259  pjhthlem2  31336  h1de2ctlem  31499  spansncol  31512  superpos  32298  cdj3lem2  32379  wrdsplex  32877  archiabllem1a  33133  archiabllem1b  33134  cmpcref  33817  ordtconnlem1  33891  gsumesum  34026  esumcst  34030  esumpcvgval  34045  sxbrsigalem2  34254  oms0  34265  omssubadd  34268  eulerpartlemt  34339  cvmsss2  35247  cvmfolem  35252  fobigcup  35874  opnregcld  36304  cldregopn  36305  onsucsuccmpi  36417  finixpnum  37585  poimirlem16  37616  poimirlem19  37619  itg2addnclem2  37652  isbnd2  37763  isbnd3  37764  totbndbnd  37769  heibor1lem  37789  heibor  37801  rngmgmbs4  37911  prnc  38047  prtlem11  38845  lsatlspsn2  38971  lsatlspsn  38972  lfl1dim  39100  lfl1dim2N  39101  lkrss2N  39148  glbconN  39356  atpointN  39722  ispsubcl2N  39926  dihglblem2aN  41272  dihglblem2N  41273  dihatexv  41317  dvh4dimat  41417  dochfl1  41455  lcfl8  41481  lcfrlem9  41529  mapdval2N  41609  mapdval4N  41611  mapdcv  41639  mapdspex  41647  hdmap14lem2a  41846  hdmap14lem6  41852  elrfi  42667  eldioph  42731  eldioph2b  42736  eldioph3  42739  eldioph4i  42785  rencldnfilem  42793  pellfund14  42871  rmxyelqirr  42883  filnm  43063  unxpwdom3  43068  lpirlnr  43090  hbt  43103  rngunsnply  43142  ofoafo  43329  naddcnffo  43337  oaun3lem1  43347  dvconstbi  44307  elrestd  45086  wessf1ornlem  45163  iccshift  45499  iooshift  45503  limcperiod  45609  sumnnodd  45611  dvnprodlem1  45927  itgperiod  45962  stirlinglem13  46067  sge0rnn0  46349  sge00  46357  fsumlesge0  46358  sge0tsms  46361  sge0cl  46362  sge0f1o  46363  sge0sup  46372  sge0resplit  46387  sge0xaddlem2  46415  sge0reuz  46428  sge0reuzb  46429  nnfoctbdjlem  46436  ovn0lem  46546  hoidmv1le  46575  hoidmvlelem1  46576  incsmflem  46722  decsmflem  46747  sigarcol  46845  7gbow  47756  0aryfvalel  48619  iscnrm3rlem2  48925