Theorem rspceeqv 3595

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2111  ∃wrex 3056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057

This theorem is referenced by:  elrnmpt1s  5898  foco2  7042  fcofo  7222  onuninsuci  7770  fo1st  7941  fo2nd  7942  onnseq  8264  nneob  8571  ecelqs  8692  resixpfo  8860  elixpsn  8861  ixpsnf1o  8862  pwfilem  9202  fofinf1o  9216  elfir  9299  inelfi  9302  fiin  9306  djur  9812  cardalephex  9981  fin23lem38  10240  fin1a2lem11  10301  fin1a2lem13  10303  reclem3pr  10940  infm3lem  12080  ccats1pfxeqrex  14622  2cshwcshw  14732  cshwcshid  14734  cshwcsh2id  14735  shftlem  14975  shftfval  14977  isercoll2  15576  infcvgaux2i  15765  mertenslem1  15791  mertenslem2  15792  fprodser  15856  bezoutlem1  16450  pcprmpw  16795  1arithlem4  16838  vdwapun  16886  vdwlem1  16893  vdwlem2  16894  vdwlem6  16898  vdwlem8  16900  elrestr  17332  gsumwspan  18754  orbsta  19225  psgneldm2i  19417  odf1o2  19485  slwhash  19536  fislw  19537  lsmelvalm  19563  pj1id  19611  efgrelexlemb  19662  cyggeninv  19795  0cyg  19805  eldprdi  19932  lss1d  20896  lspsn  20935  pwssplit1  20993  lspsneq  21059  lspprat  21090  lpi0  21263  lpi1  21264  zringcyg  21406  znf1o  21488  cygznlem3  21506  frgpcyg  21510  islindf4  21775  clsval2  22965  restcld  23087  restcldi  23088  restopnb  23090  restcls  23096  ordtbas2  23106  ordtopn1  23109  ordtopn2  23110  leordtval2  23127  iocpnfordt  23130  icomnfordt  23131  lecldbas  23134  pnrmopn  23258  cncmp  23307  fincmp  23308  cmpsublem  23314  cmpsub  23315  tgcmp  23316  uncmp  23318  cmpfi  23323  connsubclo  23339  2ndcomap  23373  dis2ndc  23375  cldllycmp  23410  dissnlocfin  23444  comppfsc  23447  ptpjopn  23527  txcmplem2  23557  qtopeu  23631  fbasrn  23799  elfm  23862  elfm3  23865  rnelfmlem  23867  rnelfm  23868  fmfnfmlem3  23871  fmfnfmlem4  23872  alexsubALTlem3  23964  ptcmplem2  23968  ptcmplem3  23969  ptcmplem5  23971  tsmsfbas  24043  trust  24144  restutopopn  24153  ustuqtop1  24156  ustuqtop2  24157  ustuqtop4  24159  ustuqtop5  24160  utopsnneiplem  24162  utopsnnei  24164  fmucnd  24206  neipcfilu  24210  mopnex  24434  metrest  24439  metustexhalf  24471  metustfbas  24472  cfilucfil  24474  restmetu  24485  metucn  24486  icoopnst  24863  iocopnst  24864  cnheibor  24881  minveclem2  25353  uniioombllem3  25513  itg1addlem4  25627  i1fmulc  25631  ply1lpir  26114  aannenlem2  26264  aalioulem2  26268  eflogeq  26538  cxpeq  26694  angpieqvd  26768  rlimcnp  26902  isppw2  27052  mpodvdsmulf1o  27131  dvdsmulf1o  27133  lgsquadlem1  27318  2sqlem2  27356  mul2sq  27357  2sqlem3  27358  2sqlem9  27365  2sqlem10  27366  ostth2  27575  ostth3  27576  bdayfo  27616  scutfo  27850  addsproplem4  27915  addsproplem5  27916  addsproplem6  27917  addsfo  27926  subsfo  28005  elons2  28195  n0seo  28344  zseo  28345  midexlem  28670  midex  28715  ttgcontlem1  28863  axcontlem7  28948  upgrex  29070  erclwwlkref  30000  clwwlkfo  30030  erclwwlknref  30049  isgrpo  30477  grpoinvf  30512  minvecolem2  30855  shsel3  31295  pjhthlem2  31372  h1de2ctlem  31535  spansncol  31548  superpos  32334  cdj3lem2  32415  wrdsplex  32917  archiabllem1a  33160  archiabllem1b  33161  cmpcref  33863  ordtconnlem1  33937  gsumesum  34072  esumcst  34076  esumpcvgval  34091  sxbrsigalem2  34299  oms0  34310  omssubadd  34313  eulerpartlemt  34384  cvmsss2  35318  cvmfolem  35323  fobigcup  35942  opnregcld  36372  cldregopn  36373  onsucsuccmpi  36485  finixpnum  37653  poimirlem16  37684  poimirlem19  37687  itg2addnclem2  37720  isbnd2  37831  isbnd3  37832  totbndbnd  37837  heibor1lem  37857  heibor  37869  rngmgmbs4  37979  prnc  38115  prtlem11  38913  lsatlspsn2  39039  lsatlspsn  39040  lfl1dim  39168  lfl1dim2N  39169  lkrss2N  39216  glbconN  39424  atpointN  39790  ispsubcl2N  39994  dihglblem2aN  41340  dihglblem2N  41341  dihatexv  41385  dvh4dimat  41485  dochfl1  41523  lcfl8  41549  lcfrlem9  41597  mapdval2N  41677  mapdval4N  41679  mapdcv  41707  mapdspex  41715  hdmap14lem2a  41914  hdmap14lem6  41920  elrfi  42735  eldioph  42799  eldioph2b  42804  eldioph3  42807  eldioph4i  42853  rencldnfilem  42861  pellfund14  42939  rmxyelqirr  42951  filnm  43131  unxpwdom3  43136  lpirlnr  43158  hbt  43171  rngunsnply  43210  ofoafo  43397  naddcnffo  43405  oaun3lem1  43415  dvconstbi  44375  elrestd  45153  wessf1ornlem  45230  iccshift  45566  iooshift  45570  limcperiod  45676  sumnnodd  45678  dvnprodlem1  45992  itgperiod  46027  stirlinglem13  46132  sge0rnn0  46414  sge00  46422  fsumlesge0  46423  sge0tsms  46426  sge0cl  46427  sge0f1o  46428  sge0sup  46437  sge0resplit  46452  sge0xaddlem2  46480  sge0reuz  46493  sge0reuzb  46494  nnfoctbdjlem  46501  ovn0lem  46611  hoidmv1le  46640  hoidmvlelem1  46641  incsmflem  46787  decsmflem  46812  sigarcol  46910  7gbow  47811  0aryfvalel  48674  iscnrm3rlem2  48980