Theorem rspceeqv 3599

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087

This theorem is used by:  elrnmpt1s  5943  foco2  7102  fcofo  7289  onuninsuci  7836  fo1st  8006  fo2nd  8007  onnseq  8333  nneob  8644  ecelqs  8767  resixpfo  8943  elixpsn  8944  ixpsnf1o  8945  pwfilem  9287  fofinf1o  9299  elfir  9385  inelfi  9388  fiin  9392  djur  9924  cardalephex  10093  fin23lem38  10351  fin1a2lem11  10412  fin1a2lem13  10414  reclem3pr  11058  infm3lem  12197  ccats1pfxeqrex  14784  2cshwcshw  14896  cshwcshid  14898  cshwcsh2id  14899  shftlem  15141  shftfval  15143  isercoll2  15756  infcvgaux2i  15947  mertenslem1  15973  mertenslem2  15974  fprodser  16036  bezoutlem1  16629  pcprmpw  16975  1arithlem4  17018  vdwapun  17066  vdwlem1  17073  vdwlem2  17074  vdwlem6  17078  vdwlem8  17080  elrestr  17513  gsumwspan  18955  orbsta  19440  psgneldm2i  19632  odf1o2  19700  slwhash  19751  fislw  19752  lsmelvalm  19778  pj1id  19826  efgrelexlemb  19877  cyggeninv  20010  0cyg  20020  eldprdi  20147  lss1d  21147  lspsn  21186  pwssplit1  21243  lspsneq  21309  lspprat  21340  lpi0  21557  lpi1  21558  zringcyg  21682  znf1o  21764  cygznlem3  21782  frgpcyg  21786  islindf4  22051  clsval2  23275  restcld  23397  restcldi  23398  restopnb  23400  restcls  23406  ordtbas2  23416  ordtopn1  23419  ordtopn2  23420  leordtval2  23437  iocpnfordt  23440  icomnfordt  23441  lecldbas  23444  pnrmopn  23568  cncmp  23617  fincmp  23618  cmpsublem  23624  cmpsub  23625  tgcmp  23626  uncmp  23628  cmpfi  23633  connsubclo  23649  2ndcomap  23684  dis2ndc  23686  cldllycmp  23721  dissnlocfin  23755  comppfsc  23758  ptpjopn  23838  txcmplem2  23868  qtopeu  23942  fbasrn  24110  elfm  24173  elfm3  24176  rnelfmlem  24178  rnelfm  24179  fmfnfmlem3  24182  fmfnfmlem4  24183  alexsubALTlem3  24275  ptcmplem2  24279  ptcmplem3  24280  ptcmplem5  24282  tsmsfbas  24354  trust  24455  restutopopn  24464  ustuqtop1  24467  ustuqtop2  24468  ustuqtop4  24470  ustuqtop5  24471  utopsnneiplem  24473  utopsnnei  24475  fmucnd  24517  neipcfilu  24521  mopnex  24745  metrest  24750  metustexhalf  24782  metustfbas  24783  cfilucfil  24785  restmetu  24796  metucn  24797  icoopnst  25167  iocopnst  25168  cnheibor  25183  minveclem2  25654  uniioombllem3  25813  itg1addlem4  25927  i1fmulc  25931  ply1lpir  26407  aannenlem2  26565  aalioulem2  26569  eflogeq  26839  cxpeq  26994  angpieqvd  27068  rlimcnp  27202  isppw2  27351  mpodvdsmulf1o  27430  dvdsmulf1o  27432  lgsquadlem1  27616  2sqlem2  27654  mul2sq  27655  2sqlem3  27656  2sqlem9  27663  2sqlem10  27664  ostth2  27873  ostth3  27874  bdayfo  27913  cutsfo  28170  addsproplem4  28237  addsproplem5  28238  addsproplem6  28239  addsfo  28248  subsfo  28330  elons2  28523  n0seo  28686  zseo  28687  midexlem  29043  midex  29092  ttgcontlem1  29341  axcontlem7  29427  upgrex  29549  erclwwlkref  30490  clwwlkfo  30520  erclwwlknref  30539  isgrpo  30978  grpoinvf  31013  minvecolem2  31356  shsel3  31796  pjhthlem2  31873  h1de2ctlem  32036  spansncol  32049  superpos  32835  cdj3lem2  32916  wrdsplex  33382  archiabllem1a  33631  archiabllem1b  33632  cmpcref  34360  ordtconnlem1  34434  gsumesum  34569  esumcst  34573  esumpcvgval  34588  sxbrsigalem2  34797  oms0  34808  omssubadd  34811  eulerpartlemt  34882  rankfo  35619  cvmsss2  35853  cvmfolem  35858  fobigcup  36477  opnregcld  36949  cldregopn  36950  onsucsuccmpi  37062  finixpnum  38359  poimirlem16  38385  poimirlem19  38388  itg2addnclem2  38421  isbnd2  38533  isbnd3  38534  totbndbnd  38539  heibor1lem  38559  heibor  38571  rngmgmbs4  38681  prnc  38817  prtlem11  39739  lsatlspsn2  39865  lsatlspsn  39866  lfl1dim  39994  lfl1dim2N  39995  lkrss2N  40042  glbconN  40250  atpointN  40616  ispsubcl2N  40820  dihglblem2aN  42166  dihglblem2N  42167  dihatexv  42211  dvh4dimat  42311  dochfl1  42349  lcfl8  42375  lcfrlem9  42423  mapdval2N  42503  mapdval4N  42505  mapdcv  42533  mapdspex  42541  hdmap14lem2a  42740  hdmap14lem6  42746  elrfi  43539  eldioph  43603  eldioph2b  43608  eldioph3  43611  eldioph4i  43653  rencldnfilem  43661  pellfund14  43739  rmxyelqirr  43751  filnm  43931  unxpwdom3  43936  lpirlnr  43958  hbt  43971  rngunsnply  44010  ofoafo  44197  naddcnffo  44205  oaun3lem1  44215  dvconstbi  45158  elrestd  45940  wessf1ornlem  46017  iccshift  46348  iooshift  46352  limcperiod  46458  sumnnodd  46460  dvnprodlem1  46774  itgperiod  46809  stirlinglem13  46914  sge0rnn0  47196  sge00  47204  fsumlesge0  47205  sge0tsms  47208  sge0cl  47209  sge0f1o  47210  sge0sup  47219  sge0resplit  47234  sge0xaddlem2  47262  sge0reuz  47275  sge0reuzb  47276  nnfoctbdjlem  47283  ovn0lem  47393  hoidmv1le  47422  hoidmvlelem1  47423  incsmflem  47569  decsmflem  47594  sigarcol  47692  7gbow  48688  0aryfvalel  49564  iscnrm3rlem2  49867