Theorem rspceeqv 3602

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 3580	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐸 = 𝐷) → ∃𝑥 ∈ 𝐵 𝐸 = 𝐶)

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091

This theorem is used by:  elrnmpt1s  5953  foco2  7141  fcofo  7327  onuninsuci  7885  fo1st  8055  fo2nd  8056  onnseq  8390  nneob  8703  ecelqs  8826  resixpfo  9002  elixpsn  9003  ixpsnf1o  9004  pwfilem  9347  fofinf1o  9359  elfir  9444  inelfi  9447  fiin  9451  djur  10037  cardalephex  10208  fin23lem38  10466  fin1a2lem11  10527  fin1a2lem13  10529  reclem3pr  11173  infm3lem  12315  ccats1pfxeqrex  14906  2cshwcshw  15018  cshwcshid  15020  cshwcsh2id  15021  shftlem  15264  shftfval  15266  isercoll2  15880  infcvgaux2i  16071  mertenslem1  16097  mertenslem2  16098  fprodser  16160  bezoutlem1  16756  pcprmpw  17105  1arithlem4  17148  vdwapun  17196  vdwlem1  17203  vdwlem2  17204  vdwlem6  17208  vdwlem8  17210  elrestr  17649  gsumwspan  19092  orbsta  19578  psgneldm2i  19770  odf1o2  19838  slwhash  19889  fislw  19890  lsmelvalm  19916  pj1id  19964  efgrelexlemb  20015  cyggeninv  20148  0cyg  20158  eldprdi  20285  lss1d  21289  lspsn  21328  pwssplit1  21385  lspsneq  21451  lspprat  21482  lpi0  21701  lpi1  21702  zringcyg  21830  znf1o  21912  cygznlem3  21930  frgpcyg  21934  islindf4  22199  clsval2  23423  restcld  23545  restcldi  23546  restopnb  23548  restcls  23554  ordtbas2  23564  ordtopn1  23567  ordtopn2  23568  leordtval2  23585  iocpnfordt  23588  icomnfordt  23589  lecldbas  23592  pnrmopn  23716  cncmp  23765  fincmp  23766  cmpsublem  23772  cmpsub  23773  tgcmp  23774  uncmp  23776  cmpfi  23781  connsubclo  23797  2ndcomap  23832  dis2ndc  23834  cldllycmp  23869  dissnlocfin  23903  comppfsc  23906  ptpjopn  23986  txcmplem2  24016  qtopeu  24090  fbasrn  24258  elfm  24321  elfm3  24324  rnelfmlem  24326  rnelfm  24327  fmfnfmlem3  24330  fmfnfmlem4  24331  alexsubALTlem3  24423  ptcmplem2  24427  ptcmplem3  24428  ptcmplem5  24430  tsmsfbas  24502  trust  24603  restutopopn  24612  ustuqtop1  24615  ustuqtop2  24616  ustuqtop4  24618  ustuqtop5  24619  utopsnneiplem  24621  utopsnnei  24623  fmucnd  24665  neipcfilu  24669  mopnex  24893  metrest  24898  metustexhalf  24930  metustfbas  24931  cfilucfil  24933  restmetu  24944  metucn  24945  icoopnst  25315  iocopnst  25316  cnheibor  25331  minveclem2  25802  uniioombllem3  25961  itg1addlem4  26075  i1fmulc  26079  ply1lpir  26555  rngunsnply  26693  aannenlem2  26713  aalioulem2  26717  eflogeq  26987  cxpeq  27142  angpieqvd  27216  rlimcnp  27350  isppw2  27499  mpodvdsmulf1o  27578  dvdsmulf1o  27580  lgsquadlem1  27764  2sqlem2  27802  mul2sq  27803  2sqlem3  27804  2sqlem9  27811  2sqlem10  27812  ostth2  28021  ostth3  28022  bdayfo  28091  cutsfo  28348  addsproplem4  28415  addsproplem5  28416  addsproplem6  28417  addsfo  28426  subsfo  28508  elons2  28701  n0seo  28864  zseo  28865  midexlem  29221  midex  29270  ttgcontlem1  29519  axcontlem7  29605  upgrex  29727  erclwwlkref  30668  clwwlkfo  30698  erclwwlknref  30717  isgrpo  31156  grpoinvf  31191  minvecolem2  31534  shsel3  31974  pjhthlem2  32051  h1de2ctlem  32214  spansncol  32227  superpos  33013  cdj3lem2  33094  wrdsplex  33599  archiabllem1a  33851  archiabllem1b  33852  cmpcref  34593  ordtconnlem1  34667  gsumesum  34802  esumcst  34806  esumpcvgval  34821  sxbrsigalem2  35029  oms0  35040  omssubadd  35043  eulerpartlemt  35114  rankfo  35858  cvmsss2  36247  cvmfolem  36252  fobigcup  36877  opnregcld  37333  cldregopn  37334  onsucsuccmpi  37446  finixpnum  38796  poimirlem16  38822  poimirlem19  38825  itg2addnclem2  38858  isbnd2  38983  isbnd3  38984  totbndbnd  38989  heibor1lem  39009  heibor  39021  rngmgmbs4  39131  prnc  39267  prtlem11  40189  lsatlspsn2  40315  lsatlspsn  40316  lfl1dim  40444  lfl1dim2N  40445  lkrss2N  40492  glbconN  40700  atpointN  41066  ispsubcl2N  41270  dihglblem2aN  42616  dihglblem2N  42617  dihatexv  42661  dvh4dimat  42761  dochfl1  42799  lcfl8  42825  lcfrlem9  42873  mapdval2N  42953  mapdval4N  42955  mapdcv  42983  mapdspex  42991  hdmap14lem2a  43190  hdmap14lem6  43196  elrfi  43971  eldioph  44035  eldioph2b  44040  eldioph3  44043  eldioph4i  44085  rencldnfilem  44093  pellfund14  44171  rmxyelqirr  44183  filnm  44358  unxpwdom3  44363  lpirlnr  44384  hbt  44397  ofoafo  44619  naddcnffo  44627  oaun3lem1  44637  dvconstbi  45579  elrestd  46396  wessf1ornlem  46473  iccshift  46803  iooshift  46807  limcperiod  46913  sumnnodd  46915  dvnprodlem1  47229  itgperiod  47264  stirlinglem13  47369  sge0rnn0  47651  sge00  47659  fsumlesge0  47660  sge0tsms  47663  sge0cl  47664  sge0f1o  47665  sge0sup  47674  sge0resplit  47689  sge0xaddlem2  47717  sge0reuz  47730  sge0reuzb  47731  nnfoctbdjlem  47738  ovn0lem  47848  hoidmv1le  47877  hoidmvlelem1  47878  incsmflem  48024  decsmflem  48049  sigarcol  48147  7gbow  49143  0aryfvalel  50077  iscnrm3rlem2  50386