Theorem rspceeqv 3644

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1536   ∈ wcel 2105  ∃wrex 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068

This theorem is referenced by:  elrnmpt1s  5972  foco2  7128  fcofo  7307  onuninsuci  7860  fo1st  8032  fo2nd  8033  onnseq  8382  nneob  8692  ecelqsg  8810  resixpfo  8974  elixpsn  8975  ixpsnf1o  8976  pwfilem  9353  fofinf1o  9369  elfir  9452  inelfi  9455  fiin  9459  djur  9956  cardalephex  10127  fin23lem38  10386  fin1a2lem11  10447  fin1a2lem13  10449  reclem3pr  11086  infm3lem  12223  ccats1pfxeqrex  14749  2cshwcshw  14860  cshwcshid  14862  cshwcsh2id  14863  shftlem  15103  shftfval  15105  isercoll2  15701  infcvgaux2i  15890  mertenslem1  15916  mertenslem2  15917  fprodser  15981  bezoutlem1  16572  pcprmpw  16916  1arithlem4  16959  vdwapun  17007  vdwlem1  17014  vdwlem2  17015  vdwlem6  17019  vdwlem8  17021  elrestr  17474  gsumwspan  18871  orbsta  19343  psgneldm2i  19537  odf1o2  19605  slwhash  19656  fislw  19657  lsmelvalm  19683  pj1id  19731  efgrelexlemb  19782  cyggeninv  19915  0cyg  19925  eldprdi  20052  lss1d  20978  lspsn  21017  pwssplit1  21075  lspsneq  21141  lspprat  21172  lpi0  21353  lpi1  21354  zringcyg  21497  znf1o  21587  cygznlem3  21605  frgpcyg  21609  islindf4  21875  clsval2  23073  restcld  23195  restcldi  23196  restopnb  23198  restcls  23204  ordtbas2  23214  ordtopn1  23217  ordtopn2  23218  leordtval2  23235  iocpnfordt  23238  icomnfordt  23239  lecldbas  23242  pnrmopn  23366  cncmp  23415  fincmp  23416  cmpsublem  23422  cmpsub  23423  tgcmp  23424  uncmp  23426  cmpfi  23431  connsubclo  23447  2ndcomap  23481  dis2ndc  23483  cldllycmp  23518  dissnlocfin  23552  comppfsc  23555  ptpjopn  23635  txcmplem2  23665  qtopeu  23739  fbasrn  23907  elfm  23970  elfm3  23973  rnelfmlem  23975  rnelfm  23976  fmfnfmlem3  23979  fmfnfmlem4  23980  alexsubALTlem3  24072  ptcmplem2  24076  ptcmplem3  24077  ptcmplem5  24079  tsmsfbas  24151  trust  24253  restutopopn  24262  ustuqtop1  24265  ustuqtop2  24266  ustuqtop4  24268  ustuqtop5  24269  utopsnneiplem  24271  utopsnnei  24273  fmucnd  24316  neipcfilu  24320  mopnex  24547  metrest  24552  metustexhalf  24584  metustfbas  24585  cfilucfil  24587  restmetu  24598  metucn  24599  icoopnst  24982  iocopnst  24983  cnheibor  25000  minveclem2  25473  uniioombllem3  25633  itg1addlem4  25747  itg1addlem4OLD  25748  i1fmulc  25752  ply1lpir  26235  aannenlem2  26385  aalioulem2  26389  eflogeq  26658  cxpeq  26814  angpieqvd  26888  rlimcnp  27022  isppw2  27172  mpodvdsmulf1o  27251  dvdsmulf1o  27253  lgsquadlem1  27438  2sqlem2  27476  mul2sq  27477  2sqlem3  27478  2sqlem9  27485  2sqlem10  27486  ostth2  27695  ostth3  27696  bdayfo  27736  scutfo  27956  addsproplem4  28019  addsproplem5  28020  addsproplem6  28021  addsfo  28030  subsfo  28109  elons2  28295  n0seo  28419  zseo  28420  midexlem  28714  midex  28759  ttgcontlem1  28913  axcontlem7  28999  upgrex  29123  erclwwlkref  30048  clwwlkfo  30078  erclwwlknref  30097  isgrpo  30525  grpoinvf  30560  minvecolem2  30903  shsel3  31343  pjhthlem2  31420  h1de2ctlem  31583  spansncol  31596  superpos  32382  cdj3lem2  32463  wrdsplex  32904  archiabllem1a  33180  archiabllem1b  33181  cmpcref  33810  ordtconnlem1  33884  gsumesum  34039  esumcst  34043  esumpcvgval  34058  sxbrsigalem2  34267  oms0  34278  omssubadd  34281  eulerpartlemt  34352  cvmsss2  35258  cvmfolem  35263  fobigcup  35881  opnregcld  36312  cldregopn  36313  onsucsuccmpi  36425  finixpnum  37591  poimirlem16  37622  poimirlem19  37625  itg2addnclem2  37658  isbnd2  37769  isbnd3  37770  totbndbnd  37775  heibor1lem  37795  heibor  37807  rngmgmbs4  37917  prnc  38053  prtlem11  38847  lsatlspsn2  38973  lsatlspsn  38974  lfl1dim  39102  lfl1dim2N  39103  lkrss2N  39150  glbconN  39358  glbconNOLD  39359  atpointN  39725  ispsubcl2N  39929  dihglblem2aN  41275  dihglblem2N  41276  dihatexv  41320  dvh4dimat  41420  dochfl1  41458  lcfl8  41484  lcfrlem9  41532  mapdval2N  41612  mapdval4N  41614  mapdcv  41642  mapdspex  41650  hdmap14lem2a  41849  hdmap14lem6  41855  elrfi  42681  eldioph  42745  eldioph2b  42750  eldioph3  42753  eldioph4i  42799  rencldnfilem  42807  pellfund14  42885  rmxyelqirr  42897  rmxyelqirrOLD  42898  filnm  43078  unxpwdom3  43083  lpirlnr  43105  hbt  43118  rngunsnply  43157  ofoafo  43345  naddcnffo  43353  oaun3lem1  43363  dvconstbi  44329  elrestd  45047  wessf1ornlem  45127  iccshift  45470  iooshift  45474  limcperiod  45583  sumnnodd  45585  dvnprodlem1  45901  itgperiod  45936  stirlinglem13  46041  sge0rnn0  46323  sge00  46331  fsumlesge0  46332  sge0tsms  46335  sge0cl  46336  sge0f1o  46337  sge0sup  46346  sge0resplit  46361  sge0xaddlem2  46389  sge0reuz  46402  sge0reuzb  46403  nnfoctbdjlem  46410  ovn0lem  46520  hoidmv1le  46549  hoidmvlelem1  46550  incsmflem  46696  decsmflem  46721  sigarcol  46819  7gbow  47696  0aryfvalel  48483  iscnrm3rlem2  48737