Theorem rspceeqv 3638

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537   ∈ wcel 2114  ∃wrex 3139

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814  df-clel 2893  df-ral 3143  df-rex 3144

This theorem is referenced by:  elrnmpt1s  5829  foco2  6873  fcofo  7044  onuninsuci  7555  fo1st  7709  fo2nd  7710  onnseq  7981  nneob  8279  ecelqsg  8352  resixpfo  8500  elixpsn  8501  ixpsnf1o  8502  fofinf1o  8799  pwfilem  8818  elfir  8879  inelfi  8882  fiin  8886  djur  9348  cardalephex  9516  fin23lem38  9771  fin1a2lem11  9832  fin1a2lem13  9834  reclem3pr  10471  infm3lem  11599  ccats1pfxeqrex  14077  2cshwcshw  14187  cshwcshid  14189  cshwcsh2id  14190  shftlem  14427  shftfval  14429  isercoll2  15025  infcvgaux2i  15213  mertenslem1  15240  mertenslem2  15241  fprodser  15303  bezoutlem1  15887  pcprmpw  16219  1arithlem4  16262  vdwapun  16310  vdwlem1  16317  vdwlem2  16318  vdwlem6  16322  vdwlem8  16324  elrestr  16702  gsumwspan  18011  orbsta  18443  psgneldm2i  18633  odf1o2  18698  slwhash  18749  fislw  18750  lsmelvalm  18776  pj1id  18825  efgrelexlemb  18876  cyggeninv  19002  0cyg  19013  eldprdi  19140  lss1d  19735  lspsn  19774  pwssplit1  19831  lspsneq  19894  lspprat  19925  lpi0  20020  lpi1  20021  zringcyg  20638  znf1o  20698  cygznlem3  20716  frgpcyg  20720  islindf4  20982  clsval2  21658  restcld  21780  restcldi  21781  restopnb  21783  restcls  21789  ordtbas2  21799  ordtopn1  21802  ordtopn2  21803  leordtval2  21820  iocpnfordt  21823  icomnfordt  21824  lecldbas  21827  pnrmopn  21951  cncmp  22000  fincmp  22001  cmpsublem  22007  cmpsub  22008  tgcmp  22009  uncmp  22011  cmpfi  22016  connsubclo  22032  2ndcomap  22066  dis2ndc  22068  cldllycmp  22103  dissnlocfin  22137  comppfsc  22140  ptpjopn  22220  txcmplem2  22250  qtopeu  22324  fbasrn  22492  elfm  22555  elfm3  22558  rnelfmlem  22560  rnelfm  22561  fmfnfmlem3  22564  fmfnfmlem4  22565  alexsubALTlem3  22657  ptcmplem2  22661  ptcmplem3  22662  ptcmplem5  22664  tsmsfbas  22736  trust  22838  restutopopn  22847  ustuqtop1  22850  ustuqtop2  22851  ustuqtop4  22853  ustuqtop5  22854  utopsnneiplem  22856  utopsnnei  22858  fmucnd  22901  neipcfilu  22905  mopnex  23129  metrest  23134  metustexhalf  23166  metustfbas  23167  cfilucfil  23169  restmetu  23180  metucn  23181  icoopnst  23543  iocopnst  23544  cnheibor  23559  minveclem2  24029  uniioombllem3  24186  itg1addlem4  24300  i1fmulc  24304  ply1lpir  24772  aannenlem2  24918  aalioulem2  24922  eflogeq  25185  cxpeq  25338  angpieqvd  25409  rlimcnp  25543  isppw2  25692  dvdsmulf1o  25771  lgsquadlem1  25956  2sqlem2  25994  mul2sq  25995  2sqlem3  25996  2sqlem9  26003  2sqlem10  26004  ostth2  26213  ostth3  26214  midexlem  26478  midex  26523  ttgcontlem1  26671  axcontlem7  26756  upgrex  26877  erclwwlkref  27798  clwwlkfo  27829  erclwwlknref  27848  isgrpo  28274  grpoinvf  28309  minvecolem2  28652  shsel3  29092  pjhthlem2  29169  h1de2ctlem  29332  spansncol  29345  superpos  30131  cdj3lem2  30212  wrdsplex  30614  archiabllem1a  30820  archiabllem1b  30821  cmpcref  31114  ordtconnlem1  31167  gsumesum  31318  esumcst  31322  esumpcvgval  31337  sxbrsigalem2  31544  oms0  31555  omssubadd  31558  eulerpartlemt  31629  cvmsss2  32521  cvmfolem  32526  bdayfo  33182  fobigcup  33361  opnregcld  33678  cldregopn  33679  onsucsuccmpi  33791  finixpnum  34892  poimirlem16  34923  poimirlem19  34926  itg2addnclem2  34959  isbnd2  35076  isbnd3  35077  totbndbnd  35082  heibor1lem  35102  heibor  35114  rngmgmbs4  35224  prnc  35360  prtlem11  36017  lsatlspsn2  36143  lsatlspsn  36144  lfl1dim  36272  lfl1dim2N  36273  lkrss2N  36320  glbconN  36528  atpointN  36894  ispsubcl2N  37098  dihglblem2aN  38444  dihglblem2N  38445  dihatexv  38489  dvh4dimat  38589  dochfl1  38627  lcfl8  38653  lcfrlem9  38701  mapdval2N  38781  mapdval4N  38783  mapdcv  38811  mapdspex  38819  hdmap14lem2a  39018  hdmap14lem6  39024  elrfi  39311  eldioph  39375  eldioph2b  39380  eldioph3  39383  eldioph4i  39429  rencldnfilem  39437  pellfund14  39515  rmxyelqirr  39527  filnm  39710  unxpwdom3  39715  lpirlnr  39737  hbt  39750  rngunsnply  39793  dvconstbi  40686  elrestd  41394  wessf1ornlem  41465  iccshift  41814  iooshift  41818  limcperiod  41929  sumnnodd  41931  dvnprodlem1  42251  itgperiod  42286  stirlinglem13  42391  sge0rnn0  42670  sge00  42678  fsumlesge0  42679  sge0tsms  42682  sge0cl  42683  sge0f1o  42684  sge0sup  42693  sge0resplit  42708  sge0xaddlem2  42736  sge0reuz  42749  sge0reuzb  42750  nnfoctbdjlem  42757  ovn0lem  42867  hoidmv1le  42896  hoidmvlelem1  42897  incsmflem  43038  decsmflem  43062  sigarcol  43141  7gbow  43957