Theorem rspceeqv 3576

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539   ∈ wcel 2107  ∃wrex 3066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071

This theorem is referenced by:  elrnmpt1s  5869  foco2  6992  fcofo  7169  onuninsuci  7696  fo1st  7860  fo2nd  7861  onnseq  8184  nneob  8495  ecelqsg  8570  resixpfo  8733  elixpsn  8734  ixpsnf1o  8735  pwfilem  8969  fofinf1o  9103  pwfilemOLD  9122  elfir  9183  inelfi  9186  fiin  9190  djur  9686  cardalephex  9855  fin23lem38  10114  fin1a2lem11  10175  fin1a2lem13  10177  reclem3pr  10814  infm3lem  11942  ccats1pfxeqrex  14437  2cshwcshw  14547  cshwcshid  14549  cshwcsh2id  14550  shftlem  14788  shftfval  14790  isercoll2  15389  infcvgaux2i  15579  mertenslem1  15605  mertenslem2  15606  fprodser  15668  bezoutlem1  16256  pcprmpw  16593  1arithlem4  16636  vdwapun  16684  vdwlem1  16691  vdwlem2  16692  vdwlem6  16696  vdwlem8  16698  elrestr  17148  gsumwspan  18494  orbsta  18928  psgneldm2i  19122  odf1o2  19187  slwhash  19238  fislw  19239  lsmelvalm  19265  pj1id  19314  efgrelexlemb  19365  cyggeninv  19492  0cyg  19503  eldprdi  19630  lss1d  20234  lspsn  20273  pwssplit1  20330  lspsneq  20393  lspprat  20424  lpi0  20527  lpi1  20528  zringcyg  20700  znf1o  20768  cygznlem3  20786  frgpcyg  20790  islindf4  21054  clsval2  22210  restcld  22332  restcldi  22333  restopnb  22335  restcls  22341  ordtbas2  22351  ordtopn1  22354  ordtopn2  22355  leordtval2  22372  iocpnfordt  22375  icomnfordt  22376  lecldbas  22379  pnrmopn  22503  cncmp  22552  fincmp  22553  cmpsublem  22559  cmpsub  22560  tgcmp  22561  uncmp  22563  cmpfi  22568  connsubclo  22584  2ndcomap  22618  dis2ndc  22620  cldllycmp  22655  dissnlocfin  22689  comppfsc  22692  ptpjopn  22772  txcmplem2  22802  qtopeu  22876  fbasrn  23044  elfm  23107  elfm3  23110  rnelfmlem  23112  rnelfm  23113  fmfnfmlem3  23116  fmfnfmlem4  23117  alexsubALTlem3  23209  ptcmplem2  23213  ptcmplem3  23214  ptcmplem5  23216  tsmsfbas  23288  trust  23390  restutopopn  23399  ustuqtop1  23402  ustuqtop2  23403  ustuqtop4  23405  ustuqtop5  23406  utopsnneiplem  23408  utopsnnei  23410  fmucnd  23453  neipcfilu  23457  mopnex  23684  metrest  23689  metustexhalf  23721  metustfbas  23722  cfilucfil  23724  restmetu  23735  metucn  23736  icoopnst  24111  iocopnst  24112  cnheibor  24127  minveclem2  24599  uniioombllem3  24758  itg1addlem4  24872  itg1addlem4OLD  24873  i1fmulc  24877  ply1lpir  25352  aannenlem2  25498  aalioulem2  25502  eflogeq  25766  cxpeq  25919  angpieqvd  25990  rlimcnp  26124  isppw2  26273  dvdsmulf1o  26352  lgsquadlem1  26537  2sqlem2  26575  mul2sq  26576  2sqlem3  26577  2sqlem9  26584  2sqlem10  26585  ostth2  26794  ostth3  26795  midexlem  27062  midex  27107  ttgcontlem1  27261  axcontlem7  27347  upgrex  27471  erclwwlkref  28393  clwwlkfo  28423  erclwwlknref  28442  isgrpo  28868  grpoinvf  28903  minvecolem2  29246  shsel3  29686  pjhthlem2  29763  h1de2ctlem  29926  spansncol  29939  superpos  30725  cdj3lem2  30806  wrdsplex  31221  archiabllem1a  31454  archiabllem1b  31455  cmpcref  31809  ordtconnlem1  31883  gsumesum  32036  esumcst  32040  esumpcvgval  32055  sxbrsigalem2  32262  oms0  32273  omssubadd  32276  eulerpartlemt  32347  cvmsss2  33245  cvmfolem  33250  bdayfo  33889  scutfo  34093  fobigcup  34211  opnregcld  34528  cldregopn  34529  onsucsuccmpi  34641  finixpnum  35771  poimirlem16  35802  poimirlem19  35805  itg2addnclem2  35838  isbnd2  35950  isbnd3  35951  totbndbnd  35956  heibor1lem  35976  heibor  35988  rngmgmbs4  36098  prnc  36234  prtlem11  36887  lsatlspsn2  37013  lsatlspsn  37014  lfl1dim  37142  lfl1dim2N  37143  lkrss2N  37190  glbconN  37398  atpointN  37764  ispsubcl2N  37968  dihglblem2aN  39314  dihglblem2N  39315  dihatexv  39359  dvh4dimat  39459  dochfl1  39497  lcfl8  39523  lcfrlem9  39571  mapdval2N  39651  mapdval4N  39653  mapdcv  39681  mapdspex  39689  hdmap14lem2a  39888  hdmap14lem6  39894  elrfi  40523  eldioph  40587  eldioph2b  40592  eldioph3  40595  eldioph4i  40641  rencldnfilem  40649  pellfund14  40727  rmxyelqirr  40739  filnm  40922  unxpwdom3  40927  lpirlnr  40949  hbt  40962  rngunsnply  41005  dvconstbi  41959  elrestd  42665  wessf1ornlem  42729  iccshift  43063  iooshift  43067  limcperiod  43176  sumnnodd  43178  dvnprodlem1  43494  itgperiod  43529  stirlinglem13  43634  sge0rnn0  43913  sge00  43921  fsumlesge0  43922  sge0tsms  43925  sge0cl  43926  sge0f1o  43927  sge0sup  43936  sge0resplit  43951  sge0xaddlem2  43979  sge0reuz  43992  sge0reuzb  43993  nnfoctbdjlem  44000  ovn0lem  44110  hoidmv1le  44139  hoidmvlelem1  44140  incsmflem  44286  decsmflem  44311  sigarcol  44391  7gbow  45235  0aryfvalel  45991  iscnrm3rlem2  46246