Theorem rspceeqv 3604

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090

This theorem is referenced by:  elrnmpt1s  5949  foco2  7104  fcofo  7286  onuninsuci  7832  fo1st  8002  fo2nd  8003  onnseq  8327  nneob  8638  ecelqs  8761  resixpfo  8930  elixpsn  8931  ixpsnf1o  8932  pwfilem  9273  fofinf1o  9285  elfir  9371  inelfi  9374  fiin  9378  djur  9901  cardalephex  10070  fin23lem38  10328  fin1a2lem11  10389  fin1a2lem13  10391  reclem3pr  11029  infm3lem  12168  ccats1pfxeqrex  14748  2cshwcshw  14858  cshwcshid  14860  cshwcsh2id  14861  shftlem  15101  shftfval  15103  isercoll2  15716  infcvgaux2i  15908  mertenslem1  15934  mertenslem2  15935  fprodser  15999  bezoutlem1  16592  pcprmpw  16938  1arithlem4  16981  vdwapun  17029  vdwlem1  17036  vdwlem2  17037  vdwlem6  17041  vdwlem8  17043  elrestr  17476  gsumwspan  18900  orbsta  19378  psgneldm2i  19570  odf1o2  19638  slwhash  19689  fislw  19690  lsmelvalm  19716  pj1id  19764  efgrelexlemb  19815  cyggeninv  19948  0cyg  19958  eldprdi  20085  lss1d  21084  lspsn  21123  pwssplit1  21180  lspsneq  21246  lspprat  21277  lpi0  21494  lpi1  21495  zringcyg  21619  znf1o  21701  cygznlem3  21719  frgpcyg  21723  islindf4  21988  clsval2  23207  restcld  23329  restcldi  23330  restopnb  23332  restcls  23338  ordtbas2  23348  ordtopn1  23351  ordtopn2  23352  leordtval2  23369  iocpnfordt  23372  icomnfordt  23373  lecldbas  23376  pnrmopn  23500  cncmp  23549  fincmp  23550  cmpsublem  23556  cmpsub  23557  tgcmp  23558  uncmp  23560  cmpfi  23565  connsubclo  23581  2ndcomap  23615  dis2ndc  23617  cldllycmp  23652  dissnlocfin  23686  comppfsc  23689  ptpjopn  23769  txcmplem2  23799  qtopeu  23873  fbasrn  24041  elfm  24104  elfm3  24107  rnelfmlem  24109  rnelfm  24110  fmfnfmlem3  24113  fmfnfmlem4  24114  alexsubALTlem3  24206  ptcmplem2  24210  ptcmplem3  24211  ptcmplem5  24213  tsmsfbas  24285  trust  24386  restutopopn  24395  ustuqtop1  24398  ustuqtop2  24399  ustuqtop4  24401  ustuqtop5  24402  utopsnneiplem  24404  utopsnnei  24406  fmucnd  24448  neipcfilu  24452  mopnex  24676  metrest  24681  metustexhalf  24713  metustfbas  24714  cfilucfil  24716  restmetu  24727  metucn  24728  icoopnst  25098  iocopnst  25099  cnheibor  25114  minveclem2  25585  uniioombllem3  25744  itg1addlem4  25858  i1fmulc  25862  ply1lpir  26339  aannenlem2  26492  aalioulem2  26496  eflogeq  26767  cxpeq  26922  angpieqvd  26996  rlimcnp  27130  isppw2  27279  mpodvdsmulf1o  27358  dvdsmulf1o  27360  lgsquadlem1  27544  2sqlem2  27582  mul2sq  27583  2sqlem3  27584  2sqlem9  27591  2sqlem10  27592  ostth2  27801  ostth3  27802  bdayfo  27841  cutsfo  28098  addsproplem4  28165  addsproplem5  28166  addsproplem6  28167  addsfo  28176  subsfo  28258  elons2  28451  n0seo  28614  zseo  28615  midexlem  28969  midex  29018  ttgcontlem1  29234  axcontlem7  29320  upgrex  29442  erclwwlkref  30371  clwwlkfo  30401  erclwwlknref  30420  isgrpo  30849  grpoinvf  30884  minvecolem2  31227  shsel3  31667  pjhthlem2  31744  h1de2ctlem  31907  spansncol  31920  superpos  32706  cdj3lem2  32787  wrdsplex  33256  archiabllem1a  33511  archiabllem1b  33512  cmpcref  34240  ordtconnlem1  34314  gsumesum  34449  esumcst  34453  esumpcvgval  34468  sxbrsigalem2  34676  oms0  34687  omssubadd  34690  eulerpartlemt  34761  rankfo  35505  cvmsss2  35766  cvmfolem  35771  fobigcup  36390  opnregcld  36841  cldregopn  36842  onsucsuccmpi  36954  finixpnum  38256  poimirlem16  38287  poimirlem19  38290  itg2addnclem2  38323  isbnd2  38434  isbnd3  38435  totbndbnd  38440  heibor1lem  38460  heibor  38472  rngmgmbs4  38582  prnc  38718  prtlem11  39640  lsatlspsn2  39766  lsatlspsn  39767  lfl1dim  39895  lfl1dim2N  39896  lkrss2N  39943  glbconN  40151  atpointN  40517  ispsubcl2N  40721  dihglblem2aN  42067  dihglblem2N  42068  dihatexv  42112  dvh4dimat  42212  dochfl1  42250  lcfl8  42276  lcfrlem9  42324  mapdval2N  42404  mapdval4N  42406  mapdcv  42434  mapdspex  42442  hdmap14lem2a  42641  hdmap14lem6  42647  elrfi  43425  eldioph  43489  eldioph2b  43494  eldioph3  43497  eldioph4i  43539  rencldnfilem  43547  pellfund14  43625  rmxyelqirr  43637  filnm  43817  unxpwdom3  43822  lpirlnr  43844  hbt  43857  rngunsnply  43896  ofoafo  44083  naddcnffo  44091  oaun3lem1  44101  dvconstbi  45044  elrestd  45826  wessf1ornlem  45903  iccshift  46234  iooshift  46238  limcperiod  46344  sumnnodd  46346  dvnprodlem1  46660  itgperiod  46695  stirlinglem13  46800  sge0rnn0  47082  sge00  47090  fsumlesge0  47091  sge0tsms  47094  sge0cl  47095  sge0f1o  47096  sge0sup  47105  sge0resplit  47120  sge0xaddlem2  47148  sge0reuz  47161  sge0reuzb  47162  nnfoctbdjlem  47169  ovn0lem  47279  hoidmv1le  47308  hoidmvlelem1  47309  incsmflem  47455  decsmflem  47480  sigarcol  47578  7gbow  48537  0aryfvalel  49414  iscnrm3rlem2  49719