Theorem rspceeqv 3597

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ∃wrex 3058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ral 3050  df-rex 3059

This theorem is referenced by:  elrnmpt1s  5906  foco2  7052  fcofo  7232  onuninsuci  7780  fo1st  7951  fo2nd  7952  onnseq  8274  nneob  8582  ecelqs  8703  resixpfo  8872  elixpsn  8873  ixpsnf1o  8874  pwfilem  9216  fofinf1o  9230  elfir  9316  inelfi  9319  fiin  9323  djur  9829  cardalephex  9998  fin23lem38  10257  fin1a2lem11  10318  fin1a2lem13  10320  reclem3pr  10958  infm3lem  12098  ccats1pfxeqrex  14636  2cshwcshw  14746  cshwcshid  14748  cshwcsh2id  14749  shftlem  14989  shftfval  14991  isercoll2  15590  infcvgaux2i  15779  mertenslem1  15805  mertenslem2  15806  fprodser  15870  bezoutlem1  16464  pcprmpw  16809  1arithlem4  16852  vdwapun  16900  vdwlem1  16907  vdwlem2  16908  vdwlem6  16912  vdwlem8  16914  elrestr  17346  gsumwspan  18769  orbsta  19240  psgneldm2i  19432  odf1o2  19500  slwhash  19551  fislw  19552  lsmelvalm  19578  pj1id  19626  efgrelexlemb  19677  cyggeninv  19810  0cyg  19820  eldprdi  19947  lss1d  20912  lspsn  20951  pwssplit1  21009  lspsneq  21075  lspprat  21106  lpi0  21279  lpi1  21280  zringcyg  21422  znf1o  21504  cygznlem3  21522  frgpcyg  21526  islindf4  21791  clsval2  22992  restcld  23114  restcldi  23115  restopnb  23117  restcls  23123  ordtbas2  23133  ordtopn1  23136  ordtopn2  23137  leordtval2  23154  iocpnfordt  23157  icomnfordt  23158  lecldbas  23161  pnrmopn  23285  cncmp  23334  fincmp  23335  cmpsublem  23341  cmpsub  23342  tgcmp  23343  uncmp  23345  cmpfi  23350  connsubclo  23366  2ndcomap  23400  dis2ndc  23402  cldllycmp  23437  dissnlocfin  23471  comppfsc  23474  ptpjopn  23554  txcmplem2  23584  qtopeu  23658  fbasrn  23826  elfm  23889  elfm3  23892  rnelfmlem  23894  rnelfm  23895  fmfnfmlem3  23898  fmfnfmlem4  23899  alexsubALTlem3  23991  ptcmplem2  23995  ptcmplem3  23996  ptcmplem5  23998  tsmsfbas  24070  trust  24171  restutopopn  24180  ustuqtop1  24183  ustuqtop2  24184  ustuqtop4  24186  ustuqtop5  24187  utopsnneiplem  24189  utopsnnei  24191  fmucnd  24233  neipcfilu  24237  mopnex  24461  metrest  24466  metustexhalf  24498  metustfbas  24499  cfilucfil  24501  restmetu  24512  metucn  24513  icoopnst  24890  iocopnst  24891  cnheibor  24908  minveclem2  25380  uniioombllem3  25540  itg1addlem4  25654  i1fmulc  25658  ply1lpir  26141  aannenlem2  26291  aalioulem2  26295  eflogeq  26565  cxpeq  26721  angpieqvd  26795  rlimcnp  26929  isppw2  27079  mpodvdsmulf1o  27158  dvdsmulf1o  27160  lgsquadlem1  27345  2sqlem2  27383  mul2sq  27384  2sqlem3  27385  2sqlem9  27392  2sqlem10  27393  ostth2  27602  ostth3  27603  bdayfo  27643  scutfo  27877  addsproplem4  27942  addsproplem5  27943  addsproplem6  27944  addsfo  27953  subsfo  28034  elons2  28226  n0seo  28379  zseo  28380  midexlem  28713  midex  28758  ttgcontlem1  28906  axcontlem7  28992  upgrex  29114  erclwwlkref  30044  clwwlkfo  30074  erclwwlknref  30093  isgrpo  30521  grpoinvf  30556  minvecolem2  30899  shsel3  31339  pjhthlem2  31416  h1de2ctlem  31579  spansncol  31592  superpos  32378  cdj3lem2  32459  wrdsplex  32967  archiabllem1a  33222  archiabllem1b  33223  cmpcref  33956  ordtconnlem1  34030  gsumesum  34165  esumcst  34169  esumpcvgval  34184  sxbrsigalem2  34392  oms0  34403  omssubadd  34406  eulerpartlemt  34477  cvmsss2  35417  cvmfolem  35422  fobigcup  36041  opnregcld  36473  cldregopn  36474  onsucsuccmpi  36586  finixpnum  37745  poimirlem16  37776  poimirlem19  37779  itg2addnclem2  37812  isbnd2  37923  isbnd3  37924  totbndbnd  37929  heibor1lem  37949  heibor  37961  rngmgmbs4  38071  prnc  38207  prtlem11  39065  lsatlspsn2  39191  lsatlspsn  39192  lfl1dim  39320  lfl1dim2N  39321  lkrss2N  39368  glbconN  39576  atpointN  39942  ispsubcl2N  40146  dihglblem2aN  41492  dihglblem2N  41493  dihatexv  41537  dvh4dimat  41637  dochfl1  41675  lcfl8  41701  lcfrlem9  41749  mapdval2N  41829  mapdval4N  41831  mapdcv  41859  mapdspex  41867  hdmap14lem2a  42066  hdmap14lem6  42072  elrfi  42878  eldioph  42942  eldioph2b  42947  eldioph3  42950  eldioph4i  42996  rencldnfilem  43004  pellfund14  43082  rmxyelqirr  43094  filnm  43274  unxpwdom3  43279  lpirlnr  43301  hbt  43314  rngunsnply  43353  ofoafo  43540  naddcnffo  43548  oaun3lem1  43558  dvconstbi  44517  elrestd  45294  wessf1ornlem  45371  iccshift  45706  iooshift  45710  limcperiod  45816  sumnnodd  45818  dvnprodlem1  46132  itgperiod  46167  stirlinglem13  46272  sge0rnn0  46554  sge00  46562  fsumlesge0  46563  sge0tsms  46566  sge0cl  46567  sge0f1o  46568  sge0sup  46577  sge0resplit  46592  sge0xaddlem2  46620  sge0reuz  46633  sge0reuzb  46634  nnfoctbdjlem  46641  ovn0lem  46751  hoidmv1le  46780  hoidmvlelem1  46781  incsmflem  46927  decsmflem  46952  sigarcol  47050  7gbow  47960  0aryfvalel  48822  iscnrm3rlem2  49128