Theorem rspceeqv 3624

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  ∃wrex 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061

This theorem is referenced by:  elrnmpt1s  5939  foco2  7098  fcofo  7280  onuninsuci  7833  fo1st  8006  fo2nd  8007  onnseq  8356  nneob  8666  ecelqsg  8784  resixpfo  8948  elixpsn  8949  ixpsnf1o  8950  pwfilem  9326  fofinf1o  9342  elfir  9425  inelfi  9428  fiin  9432  djur  9931  cardalephex  10102  fin23lem38  10361  fin1a2lem11  10422  fin1a2lem13  10424  reclem3pr  11061  infm3lem  12198  ccats1pfxeqrex  14731  2cshwcshw  14842  cshwcshid  14844  cshwcsh2id  14845  shftlem  15085  shftfval  15087  isercoll2  15683  infcvgaux2i  15872  mertenslem1  15898  mertenslem2  15899  fprodser  15963  bezoutlem1  16556  pcprmpw  16901  1arithlem4  16944  vdwapun  16992  vdwlem1  16999  vdwlem2  17000  vdwlem6  17004  vdwlem8  17006  elrestr  17440  gsumwspan  18822  orbsta  19294  psgneldm2i  19484  odf1o2  19552  slwhash  19603  fislw  19604  lsmelvalm  19630  pj1id  19678  efgrelexlemb  19729  cyggeninv  19862  0cyg  19872  eldprdi  19999  lss1d  20918  lspsn  20957  pwssplit1  21015  lspsneq  21081  lspprat  21112  lpi0  21285  lpi1  21286  zringcyg  21428  znf1o  21510  cygznlem3  21528  frgpcyg  21532  islindf4  21796  clsval2  22986  restcld  23108  restcldi  23109  restopnb  23111  restcls  23117  ordtbas2  23127  ordtopn1  23130  ordtopn2  23131  leordtval2  23148  iocpnfordt  23151  icomnfordt  23152  lecldbas  23155  pnrmopn  23279  cncmp  23328  fincmp  23329  cmpsublem  23335  cmpsub  23336  tgcmp  23337  uncmp  23339  cmpfi  23344  connsubclo  23360  2ndcomap  23394  dis2ndc  23396  cldllycmp  23431  dissnlocfin  23465  comppfsc  23468  ptpjopn  23548  txcmplem2  23578  qtopeu  23652  fbasrn  23820  elfm  23883  elfm3  23886  rnelfmlem  23888  rnelfm  23889  fmfnfmlem3  23892  fmfnfmlem4  23893  alexsubALTlem3  23985  ptcmplem2  23989  ptcmplem3  23990  ptcmplem5  23992  tsmsfbas  24064  trust  24166  restutopopn  24175  ustuqtop1  24178  ustuqtop2  24179  ustuqtop4  24181  ustuqtop5  24182  utopsnneiplem  24184  utopsnnei  24186  fmucnd  24228  neipcfilu  24232  mopnex  24456  metrest  24461  metustexhalf  24493  metustfbas  24494  cfilucfil  24496  restmetu  24507  metucn  24508  icoopnst  24885  iocopnst  24886  cnheibor  24903  minveclem2  25376  uniioombllem3  25536  itg1addlem4  25650  i1fmulc  25654  ply1lpir  26137  aannenlem2  26287  aalioulem2  26291  eflogeq  26561  cxpeq  26717  angpieqvd  26791  rlimcnp  26925  isppw2  27075  mpodvdsmulf1o  27154  dvdsmulf1o  27156  lgsquadlem1  27341  2sqlem2  27379  mul2sq  27380  2sqlem3  27381  2sqlem9  27388  2sqlem10  27389  ostth2  27598  ostth3  27599  bdayfo  27639  scutfo  27859  addsproplem4  27922  addsproplem5  27923  addsproplem6  27924  addsfo  27933  subsfo  28012  elons2  28198  n0seo  28322  zseo  28323  midexlem  28617  midex  28662  ttgcontlem1  28810  axcontlem7  28895  upgrex  29017  erclwwlkref  29947  clwwlkfo  29977  erclwwlknref  29996  isgrpo  30424  grpoinvf  30459  minvecolem2  30802  shsel3  31242  pjhthlem2  31319  h1de2ctlem  31482  spansncol  31495  superpos  32281  cdj3lem2  32362  wrdsplex  32857  archiabllem1a  33135  archiabllem1b  33136  cmpcref  33827  ordtconnlem1  33901  gsumesum  34036  esumcst  34040  esumpcvgval  34055  sxbrsigalem2  34264  oms0  34275  omssubadd  34278  eulerpartlemt  34349  cvmsss2  35242  cvmfolem  35247  fobigcup  35864  opnregcld  36294  cldregopn  36295  onsucsuccmpi  36407  finixpnum  37575  poimirlem16  37606  poimirlem19  37609  itg2addnclem2  37642  isbnd2  37753  isbnd3  37754  totbndbnd  37759  heibor1lem  37779  heibor  37791  rngmgmbs4  37901  prnc  38037  prtlem11  38830  lsatlspsn2  38956  lsatlspsn  38957  lfl1dim  39085  lfl1dim2N  39086  lkrss2N  39133  glbconN  39341  glbconNOLD  39342  atpointN  39708  ispsubcl2N  39912  dihglblem2aN  41258  dihglblem2N  41259  dihatexv  41303  dvh4dimat  41403  dochfl1  41441  lcfl8  41467  lcfrlem9  41515  mapdval2N  41595  mapdval4N  41597  mapdcv  41625  mapdspex  41633  hdmap14lem2a  41832  hdmap14lem6  41838  elrfi  42664  eldioph  42728  eldioph2b  42733  eldioph3  42736  eldioph4i  42782  rencldnfilem  42790  pellfund14  42868  rmxyelqirr  42880  rmxyelqirrOLD  42881  filnm  43061  unxpwdom3  43066  lpirlnr  43088  hbt  43101  rngunsnply  43140  ofoafo  43327  naddcnffo  43335  oaun3lem1  43345  dvconstbi  44306  elrestd  45080  wessf1ornlem  45157  iccshift  45495  iooshift  45499  limcperiod  45605  sumnnodd  45607  dvnprodlem1  45923  itgperiod  45958  stirlinglem13  46063  sge0rnn0  46345  sge00  46353  fsumlesge0  46354  sge0tsms  46357  sge0cl  46358  sge0f1o  46359  sge0sup  46368  sge0resplit  46383  sge0xaddlem2  46411  sge0reuz  46424  sge0reuzb  46425  nnfoctbdjlem  46432  ovn0lem  46542  hoidmv1le  46571  hoidmvlelem1  46572  incsmflem  46718  decsmflem  46743  sigarcol  46841  7gbow  47734  0aryfvalel  48562  iscnrm3rlem2  48863