Theorem rspceeqv 3557

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1539   ∈ wcel 2112  ∃wrex 3072

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2730

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1542  df-ex 1783  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-ral 3076  df-rex 3077

This theorem is referenced by:  elrnmpt1s  5799  foco2  6865  fcofo  7037  onuninsuci  7555  fo1st  7714  fo2nd  7715  onnseq  7992  nneob  8290  ecelqsg  8363  resixpfo  8519  elixpsn  8520  ixpsnf1o  8521  fofinf1o  8825  pwfilem  8844  elfir  8905  inelfi  8908  fiin  8912  djur  9374  cardalephex  9543  fin23lem38  9802  fin1a2lem11  9863  fin1a2lem13  9865  reclem3pr  10502  infm3lem  11628  ccats1pfxeqrex  14117  2cshwcshw  14227  cshwcshid  14229  cshwcsh2id  14230  shftlem  14468  shftfval  14470  isercoll2  15066  infcvgaux2i  15254  mertenslem1  15281  mertenslem2  15282  fprodser  15344  bezoutlem1  15931  pcprmpw  16267  1arithlem4  16310  vdwapun  16358  vdwlem1  16365  vdwlem2  16366  vdwlem6  16370  vdwlem8  16372  elrestr  16753  gsumwspan  18070  orbsta  18503  psgneldm2i  18693  odf1o2  18758  slwhash  18809  fislw  18810  lsmelvalm  18836  pj1id  18885  efgrelexlemb  18936  cyggeninv  19063  0cyg  19074  eldprdi  19201  lss1d  19796  lspsn  19835  pwssplit1  19892  lspsneq  19955  lspprat  19986  lpi0  20081  lpi1  20082  zringcyg  20252  znf1o  20312  cygznlem3  20330  frgpcyg  20334  islindf4  20596  clsval2  21743  restcld  21865  restcldi  21866  restopnb  21868  restcls  21874  ordtbas2  21884  ordtopn1  21887  ordtopn2  21888  leordtval2  21905  iocpnfordt  21908  icomnfordt  21909  lecldbas  21912  pnrmopn  22036  cncmp  22085  fincmp  22086  cmpsublem  22092  cmpsub  22093  tgcmp  22094  uncmp  22096  cmpfi  22101  connsubclo  22117  2ndcomap  22151  dis2ndc  22153  cldllycmp  22188  dissnlocfin  22222  comppfsc  22225  ptpjopn  22305  txcmplem2  22335  qtopeu  22409  fbasrn  22577  elfm  22640  elfm3  22643  rnelfmlem  22645  rnelfm  22646  fmfnfmlem3  22649  fmfnfmlem4  22650  alexsubALTlem3  22742  ptcmplem2  22746  ptcmplem3  22747  ptcmplem5  22749  tsmsfbas  22821  trust  22923  restutopopn  22932  ustuqtop1  22935  ustuqtop2  22936  ustuqtop4  22938  ustuqtop5  22939  utopsnneiplem  22941  utopsnnei  22943  fmucnd  22986  neipcfilu  22990  mopnex  23214  metrest  23219  metustexhalf  23251  metustfbas  23252  cfilucfil  23254  restmetu  23265  metucn  23266  icoopnst  23633  iocopnst  23634  cnheibor  23649  minveclem2  24119  uniioombllem3  24278  itg1addlem4  24392  i1fmulc  24396  ply1lpir  24871  aannenlem2  25017  aalioulem2  25021  eflogeq  25285  cxpeq  25438  angpieqvd  25509  rlimcnp  25643  isppw2  25792  dvdsmulf1o  25871  lgsquadlem1  26056  2sqlem2  26094  mul2sq  26095  2sqlem3  26096  2sqlem9  26103  2sqlem10  26104  ostth2  26313  ostth3  26314  midexlem  26578  midex  26623  ttgcontlem1  26771  axcontlem7  26856  upgrex  26977  erclwwlkref  27897  clwwlkfo  27927  erclwwlknref  27946  isgrpo  28372  grpoinvf  28407  minvecolem2  28750  shsel3  29190  pjhthlem2  29267  h1de2ctlem  29430  spansncol  29443  superpos  30229  cdj3lem2  30310  wrdsplex  30729  archiabllem1a  30964  archiabllem1b  30965  cmpcref  31314  ordtconnlem1  31388  gsumesum  31539  esumcst  31543  esumpcvgval  31558  sxbrsigalem2  31765  oms0  31776  omssubadd  31779  eulerpartlemt  31850  cvmsss2  32745  cvmfolem  32750  bdayfo  33438  fobigcup  33744  opnregcld  34061  cldregopn  34062  onsucsuccmpi  34174  finixpnum  35315  poimirlem16  35346  poimirlem19  35349  itg2addnclem2  35382  isbnd2  35494  isbnd3  35495  totbndbnd  35500  heibor1lem  35520  heibor  35532  rngmgmbs4  35642  prnc  35778  prtlem11  36435  lsatlspsn2  36561  lsatlspsn  36562  lfl1dim  36690  lfl1dim2N  36691  lkrss2N  36738  glbconN  36946  atpointN  37312  ispsubcl2N  37516  dihglblem2aN  38862  dihglblem2N  38863  dihatexv  38907  dvh4dimat  39007  dochfl1  39045  lcfl8  39071  lcfrlem9  39119  mapdval2N  39199  mapdval4N  39201  mapdcv  39229  mapdspex  39237  hdmap14lem2a  39436  hdmap14lem6  39442  elrfi  40001  eldioph  40065  eldioph2b  40070  eldioph3  40073  eldioph4i  40119  rencldnfilem  40127  pellfund14  40205  rmxyelqirr  40217  filnm  40400  unxpwdom3  40405  lpirlnr  40427  hbt  40440  rngunsnply  40483  dvconstbi  41404  elrestd  42110  wessf1ornlem  42174  iccshift  42514  iooshift  42518  limcperiod  42629  sumnnodd  42631  dvnprodlem1  42947  itgperiod  42982  stirlinglem13  43087  sge0rnn0  43366  sge00  43374  fsumlesge0  43375  sge0tsms  43378  sge0cl  43379  sge0f1o  43380  sge0sup  43389  sge0resplit  43404  sge0xaddlem2  43432  sge0reuz  43445  sge0reuzb  43446  nnfoctbdjlem  43453  ovn0lem  43563  hoidmv1le  43592  hoidmvlelem1  43593  incsmflem  43734  decsmflem  43758  sigarcol  43837  7gbow  44650  0aryfvalel  45406