Theorem rspceeqv 3598

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 1569   ∈ wcel 2144  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

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

This theorem is used by:  elrnmpt1s  5942  foco2  7114  fcofo  7300  onuninsuci  7855  fo1st  8025  fo2nd  8026  onnseq  8360  nneob  8673  ecelqs  8796  resixpfo  8972  elixpsn  8973  ixpsnf1o  8974  pwfilem  9317  fofinf1o  9329  elfir  9414  inelfi  9417  fiin  9421  djur  10007  cardalephex  10176  fin23lem38  10434  fin1a2lem11  10495  fin1a2lem13  10497  reclem3pr  11141  infm3lem  12282  ccats1pfxeqrex  14872  2cshwcshw  14984  cshwcshid  14986  cshwcsh2id  14987  shftlem  15230  shftfval  15232  isercoll2  15845  infcvgaux2i  16036  mertenslem1  16062  mertenslem2  16063  fprodser  16125  bezoutlem1  16721  pcprmpw  17070  1arithlem4  17113  vdwapun  17161  vdwlem1  17168  vdwlem2  17169  vdwlem6  17173  vdwlem8  17175  elrestr  17608  gsumwspan  19051  orbsta  19536  psgneldm2i  19728  odf1o2  19796  slwhash  19847  fislw  19848  lsmelvalm  19874  pj1id  19922  efgrelexlemb  19973  cyggeninv  20106  0cyg  20116  eldprdi  20243  lss1d  21247  lspsn  21286  pwssplit1  21343  lspsneq  21409  lspprat  21440  lpi0  21659  lpi1  21660  zringcyg  21784  znf1o  21866  cygznlem3  21884  frgpcyg  21888  islindf4  22153  clsval2  23377  restcld  23499  restcldi  23500  restopnb  23502  restcls  23508  ordtbas2  23518  ordtopn1  23521  ordtopn2  23522  leordtval2  23539  iocpnfordt  23542  icomnfordt  23543  lecldbas  23546  pnrmopn  23670  cncmp  23719  fincmp  23720  cmpsublem  23726  cmpsub  23727  tgcmp  23728  uncmp  23730  cmpfi  23735  connsubclo  23751  2ndcomap  23786  dis2ndc  23788  cldllycmp  23823  dissnlocfin  23857  comppfsc  23860  ptpjopn  23940  txcmplem2  23970  qtopeu  24044  fbasrn  24212  elfm  24275  elfm3  24278  rnelfmlem  24280  rnelfm  24281  fmfnfmlem3  24284  fmfnfmlem4  24285  alexsubALTlem3  24377  ptcmplem2  24381  ptcmplem3  24382  ptcmplem5  24384  tsmsfbas  24456  trust  24557  restutopopn  24566  ustuqtop1  24569  ustuqtop2  24570  ustuqtop4  24572  ustuqtop5  24573  utopsnneiplem  24575  utopsnnei  24577  fmucnd  24619  neipcfilu  24623  mopnex  24847  metrest  24852  metustexhalf  24884  metustfbas  24885  cfilucfil  24887  restmetu  24898  metucn  24899  icoopnst  25269  iocopnst  25270  cnheibor  25285  minveclem2  25756  uniioombllem3  25915  itg1addlem4  26029  i1fmulc  26033  ply1lpir  26509  aannenlem2  26665  aalioulem2  26669  eflogeq  26939  cxpeq  27094  angpieqvd  27168  rlimcnp  27302  isppw2  27451  mpodvdsmulf1o  27530  dvdsmulf1o  27532  lgsquadlem1  27716  2sqlem2  27754  mul2sq  27755  2sqlem3  27756  2sqlem9  27763  2sqlem10  27764  ostth2  27973  ostth3  27974  bdayfo  28043  cutsfo  28300  addsproplem4  28367  addsproplem5  28368  addsproplem6  28369  addsfo  28378  subsfo  28460  elons2  28653  n0seo  28816  zseo  28817  midexlem  29173  midex  29222  ttgcontlem1  29471  axcontlem7  29557  upgrex  29679  erclwwlkref  30620  clwwlkfo  30650  erclwwlknref  30669  isgrpo  31108  grpoinvf  31143  minvecolem2  31486  shsel3  31926  pjhthlem2  32003  h1de2ctlem  32166  spansncol  32179  superpos  32965  cdj3lem2  33046  wrdsplex  33553  archiabllem1a  33802  archiabllem1b  33803  cmpcref  34532  ordtconnlem1  34606  gsumesum  34741  esumcst  34745  esumpcvgval  34760  sxbrsigalem2  34968  oms0  34979  omssubadd  34982  eulerpartlemt  35053  rankfo  35793  cvmsss2  36157  cvmfolem  36162  fobigcup  36786  opnregcld  37242  cldregopn  37243  onsucsuccmpi  37355  finixpnum  38665  poimirlem16  38691  poimirlem19  38694  itg2addnclem2  38727  isbnd2  38854  isbnd3  38855  totbndbnd  38860  heibor1lem  38880  heibor  38892  rngmgmbs4  39002  prnc  39138  prtlem11  40060  lsatlspsn2  40186  lsatlspsn  40187  lfl1dim  40315  lfl1dim2N  40316  lkrss2N  40363  glbconN  40571  atpointN  40937  ispsubcl2N  41141  dihglblem2aN  42487  dihglblem2N  42488  dihatexv  42532  dvh4dimat  42632  dochfl1  42670  lcfl8  42696  lcfrlem9  42744  mapdval2N  42824  mapdval4N  42826  mapdcv  42854  mapdspex  42862  hdmap14lem2a  43061  hdmap14lem6  43067  elrfi  43842  eldioph  43906  eldioph2b  43911  eldioph3  43914  eldioph4i  43956  rencldnfilem  43964  pellfund14  44042  rmxyelqirr  44054  filnm  44229  unxpwdom3  44234  lpirlnr  44256  hbt  44269  rngunsnply  44308  ofoafo  44495  naddcnffo  44503  oaun3lem1  44513  dvconstbi  45455  elrestd  46259  wessf1ornlem  46336  iccshift  46666  iooshift  46670  limcperiod  46776  sumnnodd  46778  dvnprodlem1  47092  itgperiod  47127  stirlinglem13  47232  sge0rnn0  47514  sge00  47522  fsumlesge0  47523  sge0tsms  47526  sge0cl  47527  sge0f1o  47528  sge0sup  47537  sge0resplit  47552  sge0xaddlem2  47580  sge0reuz  47593  sge0reuzb  47594  nnfoctbdjlem  47601  ovn0lem  47711  hoidmv1le  47740  hoidmvlelem1  47741  incsmflem  47887  decsmflem  47912  sigarcol  48010  7gbow  49006  0aryfvalel  49882  iscnrm3rlem2  50191