Theorem rspceeqv 3633

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  ∃wrex 3070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071

This theorem is referenced by:  elrnmpt1s  5956  foco2  7108  fcofo  7285  onuninsuci  7828  fo1st  7994  fo2nd  7995  onnseq  8343  nneob  8654  ecelqsg  8765  resixpfo  8929  elixpsn  8930  ixpsnf1o  8931  pwfilem  9176  fofinf1o  9326  pwfilemOLD  9345  elfir  9409  inelfi  9412  fiin  9416  djur  9913  cardalephex  10084  fin23lem38  10343  fin1a2lem11  10404  fin1a2lem13  10406  reclem3pr  11043  infm3lem  12171  ccats1pfxeqrex  14664  2cshwcshw  14775  cshwcshid  14777  cshwcsh2id  14778  shftlem  15014  shftfval  15016  isercoll2  15614  infcvgaux2i  15803  mertenslem1  15829  mertenslem2  15830  fprodser  15892  bezoutlem1  16480  pcprmpw  16815  1arithlem4  16858  vdwapun  16906  vdwlem1  16913  vdwlem2  16914  vdwlem6  16918  vdwlem8  16920  elrestr  17373  gsumwspan  18726  orbsta  19176  psgneldm2i  19372  odf1o2  19440  slwhash  19491  fislw  19492  lsmelvalm  19518  pj1id  19566  efgrelexlemb  19617  cyggeninv  19750  0cyg  19760  eldprdi  19887  lss1d  20573  lspsn  20612  pwssplit1  20669  lspsneq  20734  lspprat  20765  lpi0  20884  lpi1  20885  zringcyg  21038  znf1o  21106  cygznlem3  21124  frgpcyg  21128  islindf4  21392  clsval2  22553  restcld  22675  restcldi  22676  restopnb  22678  restcls  22684  ordtbas2  22694  ordtopn1  22697  ordtopn2  22698  leordtval2  22715  iocpnfordt  22718  icomnfordt  22719  lecldbas  22722  pnrmopn  22846  cncmp  22895  fincmp  22896  cmpsublem  22902  cmpsub  22903  tgcmp  22904  uncmp  22906  cmpfi  22911  connsubclo  22927  2ndcomap  22961  dis2ndc  22963  cldllycmp  22998  dissnlocfin  23032  comppfsc  23035  ptpjopn  23115  txcmplem2  23145  qtopeu  23219  fbasrn  23387  elfm  23450  elfm3  23453  rnelfmlem  23455  rnelfm  23456  fmfnfmlem3  23459  fmfnfmlem4  23460  alexsubALTlem3  23552  ptcmplem2  23556  ptcmplem3  23557  ptcmplem5  23559  tsmsfbas  23631  trust  23733  restutopopn  23742  ustuqtop1  23745  ustuqtop2  23746  ustuqtop4  23748  ustuqtop5  23749  utopsnneiplem  23751  utopsnnei  23753  fmucnd  23796  neipcfilu  23800  mopnex  24027  metrest  24032  metustexhalf  24064  metustfbas  24065  cfilucfil  24067  restmetu  24078  metucn  24079  icoopnst  24454  iocopnst  24455  cnheibor  24470  minveclem2  24942  uniioombllem3  25101  itg1addlem4  25215  itg1addlem4OLD  25216  i1fmulc  25220  ply1lpir  25695  aannenlem2  25841  aalioulem2  25845  eflogeq  26109  cxpeq  26262  angpieqvd  26333  rlimcnp  26467  isppw2  26616  dvdsmulf1o  26695  lgsquadlem1  26880  2sqlem2  26918  mul2sq  26919  2sqlem3  26920  2sqlem9  26927  2sqlem10  26928  ostth2  27137  ostth3  27138  bdayfo  27177  scutfo  27395  addsproplem4  27453  addsproplem5  27454  addsproplem6  27455  addsfo  27464  midexlem  27940  midex  27985  ttgcontlem1  28139  axcontlem7  28225  upgrex  28349  erclwwlkref  29270  clwwlkfo  29300  erclwwlknref  29319  isgrpo  29745  grpoinvf  29780  minvecolem2  30123  shsel3  30563  pjhthlem2  30640  h1de2ctlem  30803  spansncol  30816  superpos  31602  cdj3lem2  31683  wrdsplex  32099  archiabllem1a  32332  archiabllem1b  32333  cmpcref  32825  ordtconnlem1  32899  gsumesum  33052  esumcst  33056  esumpcvgval  33071  sxbrsigalem2  33280  oms0  33291  omssubadd  33294  eulerpartlemt  33365  cvmsss2  34260  cvmfolem  34265  fobigcup  34867  opnregcld  35210  cldregopn  35211  onsucsuccmpi  35323  finixpnum  36468  poimirlem16  36499  poimirlem19  36502  itg2addnclem2  36535  isbnd2  36646  isbnd3  36647  totbndbnd  36652  heibor1lem  36672  heibor  36684  rngmgmbs4  36794  prnc  36930  prtlem11  37731  lsatlspsn2  37857  lsatlspsn  37858  lfl1dim  37986  lfl1dim2N  37987  lkrss2N  38034  glbconN  38242  glbconNOLD  38243  atpointN  38609  ispsubcl2N  38813  dihglblem2aN  40159  dihglblem2N  40160  dihatexv  40204  dvh4dimat  40304  dochfl1  40342  lcfl8  40368  lcfrlem9  40416  mapdval2N  40496  mapdval4N  40498  mapdcv  40526  mapdspex  40534  hdmap14lem2a  40733  hdmap14lem6  40739  elrfi  41422  eldioph  41486  eldioph2b  41491  eldioph3  41494  eldioph4i  41540  rencldnfilem  41548  pellfund14  41626  rmxyelqirr  41638  rmxyelqirrOLD  41639  filnm  41822  unxpwdom3  41827  lpirlnr  41849  hbt  41862  rngunsnply  41905  ofoafo  42096  naddcnffo  42104  oaun3lem1  42114  dvconstbi  43083  elrestd  43787  wessf1ornlem  43872  iccshift  44221  iooshift  44225  limcperiod  44334  sumnnodd  44336  dvnprodlem1  44652  itgperiod  44687  stirlinglem13  44792  sge0rnn0  45074  sge00  45082  fsumlesge0  45083  sge0tsms  45086  sge0cl  45087  sge0f1o  45088  sge0sup  45097  sge0resplit  45112  sge0xaddlem2  45140  sge0reuz  45153  sge0reuzb  45154  nnfoctbdjlem  45161  ovn0lem  45271  hoidmv1le  45300  hoidmvlelem1  45301  incsmflem  45447  decsmflem  45472  sigarcol  45570  7gbow  46430  0aryfvalel  47310  iscnrm3rlem2  47564