Theorem rspceeqv 3613

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567   ∈ wcel 2149  ∃wrex 3095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096

This theorem is referenced by:  elrnmpt1s  5950  foco2  7105  fcofo  7287  onuninsuci  7835  fo1st  8005  fo2nd  8006  onnseq  8330  nneob  8641  ecelqs  8764  resixpfo  8933  elixpsn  8934  ixpsnf1o  8935  pwfilem  9276  fofinf1o  9288  elfir  9374  inelfi  9377  fiin  9381  djur  9904  cardalephex  10073  fin23lem38  10332  fin1a2lem11  10393  fin1a2lem13  10395  reclem3pr  11033  infm3lem  12172  ccats1pfxeqrex  14751  2cshwcshw  14861  cshwcshid  14863  cshwcsh2id  14864  shftlem  15104  shftfval  15106  isercoll2  15719  infcvgaux2i  15911  mertenslem1  15937  mertenslem2  15938  fprodser  16002  bezoutlem1  16596  pcprmpw  16942  1arithlem4  16985  vdwapun  17033  vdwlem1  17040  vdwlem2  17041  vdwlem6  17045  vdwlem8  17047  elrestr  17480  gsumwspan  18904  orbsta  19382  psgneldm2i  19574  odf1o2  19642  slwhash  19693  fislw  19694  lsmelvalm  19720  pj1id  19768  efgrelexlemb  19819  cyggeninv  19952  0cyg  19962  eldprdi  20089  lss1d  21061  lspsn  21100  pwssplit1  21157  lspsneq  21223  lspprat  21254  lpi0  21462  lpi1  21463  zringcyg  21587  znf1o  21669  cygznlem3  21687  frgpcyg  21691  islindf4  21956  clsval2  23175  restcld  23297  restcldi  23298  restopnb  23300  restcls  23306  ordtbas2  23316  ordtopn1  23319  ordtopn2  23320  leordtval2  23337  iocpnfordt  23340  icomnfordt  23341  lecldbas  23344  pnrmopn  23468  cncmp  23517  fincmp  23518  cmpsublem  23524  cmpsub  23525  tgcmp  23526  uncmp  23528  cmpfi  23533  connsubclo  23549  2ndcomap  23583  dis2ndc  23585  cldllycmp  23620  dissnlocfin  23654  comppfsc  23657  ptpjopn  23737  txcmplem2  23767  qtopeu  23841  fbasrn  24009  elfm  24072  elfm3  24075  rnelfmlem  24077  rnelfm  24078  fmfnfmlem3  24081  fmfnfmlem4  24082  alexsubALTlem3  24174  ptcmplem2  24178  ptcmplem3  24179  ptcmplem5  24181  tsmsfbas  24253  trust  24354  restutopopn  24363  ustuqtop1  24366  ustuqtop2  24367  ustuqtop4  24369  ustuqtop5  24370  utopsnneiplem  24372  utopsnnei  24374  fmucnd  24416  neipcfilu  24420  mopnex  24644  metrest  24649  metustexhalf  24681  metustfbas  24682  cfilucfil  24684  restmetu  24695  metucn  24696  icoopnst  25066  iocopnst  25067  cnheibor  25082  minveclem2  25553  uniioombllem3  25712  itg1addlem4  25826  i1fmulc  25830  ply1lpir  26307  aannenlem2  26458  aalioulem2  26462  eflogeq  26732  cxpeq  26887  angpieqvd  26961  rlimcnp  27095  isppw2  27244  mpodvdsmulf1o  27323  dvdsmulf1o  27325  lgsquadlem1  27509  2sqlem2  27547  mul2sq  27548  2sqlem3  27549  2sqlem9  27556  2sqlem10  27557  ostth2  27766  ostth3  27767  bdayfo  27806  cutsfo  28063  addsproplem4  28130  addsproplem5  28131  addsproplem6  28132  addsfo  28141  subsfo  28223  elons2  28416  n0seo  28579  zseo  28580  midexlem  28930  midex  28976  ttgcontlem1  29174  axcontlem7  29260  upgrex  29382  erclwwlkref  30311  clwwlkfo  30341  erclwwlknref  30360  isgrpo  30789  grpoinvf  30824  minvecolem2  31167  shsel3  31607  pjhthlem2  31684  h1de2ctlem  31847  spansncol  31860  superpos  32646  cdj3lem2  32727  wrdsplex  33196  archiabllem1a  33451  archiabllem1b  33452  cmpcref  34184  ordtconnlem1  34258  gsumesum  34393  esumcst  34397  esumpcvgval  34412  sxbrsigalem2  34620  oms0  34631  omssubadd  34634  eulerpartlemt  34705  cvmsss2  35664  cvmfolem  35669  fobigcup  36288  opnregcld  36729  cldregopn  36730  onsucsuccmpi  36842  finixpnum  38143  poimirlem16  38174  poimirlem19  38177  itg2addnclem2  38210  isbnd2  38321  isbnd3  38322  totbndbnd  38327  heibor1lem  38347  heibor  38359  rngmgmbs4  38469  prnc  38605  prtlem11  39529  lsatlspsn2  39655  lsatlspsn  39656  lfl1dim  39784  lfl1dim2N  39785  lkrss2N  39832  glbconN  40040  atpointN  40406  ispsubcl2N  40610  dihglblem2aN  41956  dihglblem2N  41957  dihatexv  42001  dvh4dimat  42101  dochfl1  42139  lcfl8  42165  lcfrlem9  42213  mapdval2N  42293  mapdval4N  42295  mapdcv  42323  mapdspex  42331  hdmap14lem2a  42530  hdmap14lem6  42536  elrfi  43316  eldioph  43380  eldioph2b  43385  eldioph3  43388  eldioph4i  43430  rencldnfilem  43438  pellfund14  43516  rmxyelqirr  43528  filnm  43708  unxpwdom3  43713  lpirlnr  43735  hbt  43748  rngunsnply  43787  ofoafo  43974  naddcnffo  43982  oaun3lem1  43992  dvconstbi  44935  elrestd  45717  wessf1ornlem  45794  iccshift  46125  iooshift  46129  limcperiod  46235  sumnnodd  46237  dvnprodlem1  46551  itgperiod  46586  stirlinglem13  46691  sge0rnn0  46973  sge00  46981  fsumlesge0  46982  sge0tsms  46985  sge0cl  46986  sge0f1o  46987  sge0sup  46996  sge0resplit  47011  sge0xaddlem2  47039  sge0reuz  47052  sge0reuzb  47053  nnfoctbdjlem  47060  ovn0lem  47170  hoidmv1le  47199  hoidmvlelem1  47200  incsmflem  47346  decsmflem  47371  sigarcol  47469  7gbow  48425  0aryfvalel  49298  iscnrm3rlem2  49603