Theorem rspceeqv 3631

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

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107  ∃wrex 3071

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072

This theorem is referenced by:  elrnmpt1s  5951  foco2  7096  fcofo  7273  onuninsuci  7816  fo1st  7982  fo2nd  7983  onnseq  8331  nneob  8643  ecelqsg  8754  resixpfo  8918  elixpsn  8919  ixpsnf1o  8920  pwfilem  9165  fofinf1o  9315  pwfilemOLD  9334  elfir  9397  inelfi  9400  fiin  9404  djur  9901  cardalephex  10072  fin23lem38  10331  fin1a2lem11  10392  fin1a2lem13  10394  reclem3pr  11031  infm3lem  12159  ccats1pfxeqrex  14652  2cshwcshw  14763  cshwcshid  14765  cshwcsh2id  14766  shftlem  15002  shftfval  15004  isercoll2  15602  infcvgaux2i  15791  mertenslem1  15817  mertenslem2  15818  fprodser  15880  bezoutlem1  16468  pcprmpw  16803  1arithlem4  16846  vdwapun  16894  vdwlem1  16901  vdwlem2  16902  vdwlem6  16906  vdwlem8  16908  elrestr  17361  gsumwspan  18714  orbsta  19162  psgneldm2i  19357  odf1o2  19425  slwhash  19476  fislw  19477  lsmelvalm  19503  pj1id  19551  efgrelexlemb  19602  cyggeninv  19734  0cyg  19744  eldprdi  19871  lss1d  20551  lspsn  20590  pwssplit1  20647  lspsneq  20712  lspprat  20743  lpi0  20861  lpi1  20862  zringcyg  21012  znf1o  21080  cygznlem3  21098  frgpcyg  21102  islindf4  21366  clsval2  22523  restcld  22645  restcldi  22646  restopnb  22648  restcls  22654  ordtbas2  22664  ordtopn1  22667  ordtopn2  22668  leordtval2  22685  iocpnfordt  22688  icomnfordt  22689  lecldbas  22692  pnrmopn  22816  cncmp  22865  fincmp  22866  cmpsublem  22872  cmpsub  22873  tgcmp  22874  uncmp  22876  cmpfi  22881  connsubclo  22897  2ndcomap  22931  dis2ndc  22933  cldllycmp  22968  dissnlocfin  23002  comppfsc  23005  ptpjopn  23085  txcmplem2  23115  qtopeu  23189  fbasrn  23357  elfm  23420  elfm3  23423  rnelfmlem  23425  rnelfm  23426  fmfnfmlem3  23429  fmfnfmlem4  23430  alexsubALTlem3  23522  ptcmplem2  23526  ptcmplem3  23527  ptcmplem5  23529  tsmsfbas  23601  trust  23703  restutopopn  23712  ustuqtop1  23715  ustuqtop2  23716  ustuqtop4  23718  ustuqtop5  23719  utopsnneiplem  23721  utopsnnei  23723  fmucnd  23766  neipcfilu  23770  mopnex  23997  metrest  24002  metustexhalf  24034  metustfbas  24035  cfilucfil  24037  restmetu  24048  metucn  24049  icoopnst  24424  iocopnst  24425  cnheibor  24440  minveclem2  24912  uniioombllem3  25071  itg1addlem4  25185  itg1addlem4OLD  25186  i1fmulc  25190  ply1lpir  25665  aannenlem2  25811  aalioulem2  25815  eflogeq  26079  cxpeq  26232  angpieqvd  26303  rlimcnp  26437  isppw2  26586  dvdsmulf1o  26665  lgsquadlem1  26850  2sqlem2  26888  mul2sq  26889  2sqlem3  26890  2sqlem9  26897  2sqlem10  26898  ostth2  27107  ostth3  27108  bdayfo  27147  scutfo  27365  addsproplem4  27423  addsproplem5  27424  addsproplem6  27425  addsfo  27434  midexlem  27910  midex  27955  ttgcontlem1  28109  axcontlem7  28195  upgrex  28319  erclwwlkref  29240  clwwlkfo  29270  erclwwlknref  29289  isgrpo  29715  grpoinvf  29750  minvecolem2  30093  shsel3  30533  pjhthlem2  30610  h1de2ctlem  30773  spansncol  30786  superpos  31572  cdj3lem2  31653  wrdsplex  32075  archiabllem1a  32308  archiabllem1b  32309  cmpcref  32761  ordtconnlem1  32835  gsumesum  32988  esumcst  32992  esumpcvgval  33007  sxbrsigalem2  33216  oms0  33227  omssubadd  33230  eulerpartlemt  33301  cvmsss2  34196  cvmfolem  34201  fobigcup  34803  opnregcld  35120  cldregopn  35121  onsucsuccmpi  35233  finixpnum  36378  poimirlem16  36409  poimirlem19  36412  itg2addnclem2  36445  isbnd2  36557  isbnd3  36558  totbndbnd  36563  heibor1lem  36583  heibor  36595  rngmgmbs4  36705  prnc  36841  prtlem11  37642  lsatlspsn2  37768  lsatlspsn  37769  lfl1dim  37897  lfl1dim2N  37898  lkrss2N  37945  glbconN  38153  glbconNOLD  38154  atpointN  38520  ispsubcl2N  38724  dihglblem2aN  40070  dihglblem2N  40071  dihatexv  40115  dvh4dimat  40215  dochfl1  40253  lcfl8  40279  lcfrlem9  40327  mapdval2N  40407  mapdval4N  40409  mapdcv  40437  mapdspex  40445  hdmap14lem2a  40644  hdmap14lem6  40650  elrfi  41303  eldioph  41367  eldioph2b  41372  eldioph3  41375  eldioph4i  41421  rencldnfilem  41429  pellfund14  41507  rmxyelqirr  41519  rmxyelqirrOLD  41520  filnm  41703  unxpwdom3  41708  lpirlnr  41730  hbt  41743  rngunsnply  41786  ofoafo  41977  naddcnffo  41985  oaun3lem1  41995  dvconstbi  42964  elrestd  43668  wessf1ornlem  43753  iccshift  44104  iooshift  44108  limcperiod  44217  sumnnodd  44219  dvnprodlem1  44535  itgperiod  44570  stirlinglem13  44675  sge0rnn0  44957  sge00  44965  fsumlesge0  44966  sge0tsms  44969  sge0cl  44970  sge0f1o  44971  sge0sup  44980  sge0resplit  44995  sge0xaddlem2  45023  sge0reuz  45036  sge0reuzb  45037  nnfoctbdjlem  45044  ovn0lem  45154  hoidmv1le  45183  hoidmvlelem1  45184  incsmflem  45330  decsmflem  45355  sigarcol  45453  7gbow  46313  0aryfvalel  47160  iscnrm3rlem2  47414