Theorem rspceeqv 3604

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1560   ∈ wcel 2142  ∃wrex 3086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3077  df-rex 3087

This theorem is referenced by:  elrnmpt1s  5935  foco2  7090  fcofo  7272  onuninsuci  7820  fo1st  7990  fo2nd  7991  onnseq  8315  nneob  8626  ecelqs  8749  resixpfo  8918  elixpsn  8919  ixpsnf1o  8920  pwfilem  9262  fofinf1o  9275  elfir  9361  inelfi  9364  fiin  9368  djur  9877  cardalephex  10046  fin23lem38  10306  fin1a2lem11  10367  fin1a2lem13  10369  reclem3pr  11007  infm3lem  12150  ccats1pfxeqrex  14728  2cshwcshw  14838  cshwcshid  14840  cshwcsh2id  14841  shftlem  15081  shftfval  15083  isercoll2  15696  infcvgaux2i  15888  mertenslem1  15914  mertenslem2  15915  fprodser  15979  bezoutlem1  16573  pcprmpw  16919  1arithlem4  16962  vdwapun  17010  vdwlem1  17017  vdwlem2  17018  vdwlem6  17022  vdwlem8  17024  elrestr  17457  gsumwspan  18880  orbsta  19353  psgneldm2i  19545  odf1o2  19613  slwhash  19664  fislw  19665  lsmelvalm  19691  pj1id  19739  efgrelexlemb  19790  cyggeninv  19923  0cyg  19933  eldprdi  20060  lss1d  21030  lspsn  21069  pwssplit1  21126  lspsneq  21192  lspprat  21223  lpi0  21396  lpi1  21397  zringcyg  21521  znf1o  21603  cygznlem3  21621  frgpcyg  21625  islindf4  21890  clsval2  23110  restcld  23232  restcldi  23233  restopnb  23235  restcls  23241  ordtbas2  23251  ordtopn1  23254  ordtopn2  23255  leordtval2  23272  iocpnfordt  23275  icomnfordt  23276  lecldbas  23279  pnrmopn  23403  cncmp  23452  fincmp  23453  cmpsublem  23459  cmpsub  23460  tgcmp  23461  uncmp  23463  cmpfi  23468  connsubclo  23484  2ndcomap  23518  dis2ndc  23520  cldllycmp  23555  dissnlocfin  23589  comppfsc  23592  ptpjopn  23672  txcmplem2  23702  qtopeu  23776  fbasrn  23944  elfm  24007  elfm3  24010  rnelfmlem  24012  rnelfm  24013  fmfnfmlem3  24016  fmfnfmlem4  24017  alexsubALTlem3  24109  ptcmplem2  24113  ptcmplem3  24114  ptcmplem5  24116  tsmsfbas  24188  trust  24289  restutopopn  24298  ustuqtop1  24301  ustuqtop2  24302  ustuqtop4  24304  ustuqtop5  24305  utopsnneiplem  24307  utopsnnei  24309  fmucnd  24351  neipcfilu  24355  mopnex  24579  metrest  24584  metustexhalf  24616  metustfbas  24617  cfilucfil  24619  restmetu  24630  metucn  24631  icoopnst  25001  iocopnst  25002  cnheibor  25017  minveclem2  25488  uniioombllem3  25647  itg1addlem4  25761  i1fmulc  25765  ply1lpir  26242  aannenlem2  26393  aalioulem2  26397  eflogeq  26667  cxpeq  26822  angpieqvd  26896  rlimcnp  27030  isppw2  27179  mpodvdsmulf1o  27258  dvdsmulf1o  27260  lgsquadlem1  27444  2sqlem2  27482  mul2sq  27483  2sqlem3  27484  2sqlem9  27491  2sqlem10  27492  ostth2  27701  ostth3  27702  bdayfo  27741  cutsfo  27998  addsproplem4  28065  addsproplem5  28066  addsproplem6  28067  addsfo  28076  subsfo  28158  elons2  28351  n0seo  28514  zseo  28515  midexlem  28865  midex  28910  ttgcontlem1  29085  axcontlem7  29171  upgrex  29293  erclwwlkref  30222  clwwlkfo  30252  erclwwlknref  30271  isgrpo  30700  grpoinvf  30735  minvecolem2  31078  shsel3  31518  pjhthlem2  31595  h1de2ctlem  31758  spansncol  31771  superpos  32557  cdj3lem2  32638  wrdsplex  33114  archiabllem1a  33371  archiabllem1b  33372  cmpcref  34147  ordtconnlem1  34221  gsumesum  34356  esumcst  34360  esumpcvgval  34375  sxbrsigalem2  34583  oms0  34594  omssubadd  34597  eulerpartlemt  34668  cvmsss2  35624  cvmfolem  35629  fobigcup  36248  opnregcld  36690  cldregopn  36691  onsucsuccmpi  36803  finixpnum  38104  poimirlem16  38135  poimirlem19  38138  itg2addnclem2  38171  isbnd2  38282  isbnd3  38283  totbndbnd  38288  heibor1lem  38308  heibor  38320  rngmgmbs4  38430  prnc  38566  prtlem11  39490  lsatlspsn2  39616  lsatlspsn  39617  lfl1dim  39745  lfl1dim2N  39746  lkrss2N  39793  glbconN  40001  atpointN  40367  ispsubcl2N  40571  dihglblem2aN  41917  dihglblem2N  41918  dihatexv  41962  dvh4dimat  42062  dochfl1  42100  lcfl8  42126  lcfrlem9  42174  mapdval2N  42254  mapdval4N  42256  mapdcv  42284  mapdspex  42292  hdmap14lem2a  42491  hdmap14lem6  42497  elrfi  43275  eldioph  43339  eldioph2b  43344  eldioph3  43347  eldioph4i  43389  rencldnfilem  43397  pellfund14  43475  rmxyelqirr  43487  filnm  43667  unxpwdom3  43672  lpirlnr  43694  hbt  43707  rngunsnply  43746  ofoafo  43933  naddcnffo  43941  oaun3lem1  43951  dvconstbi  44910  elrestd  45686  wessf1ornlem  45763  iccshift  46094  iooshift  46098  limcperiod  46204  sumnnodd  46206  dvnprodlem1  46520  itgperiod  46555  stirlinglem13  46660  sge0rnn0  46942  sge00  46950  fsumlesge0  46951  sge0tsms  46954  sge0cl  46955  sge0f1o  46956  sge0sup  46965  sge0resplit  46980  sge0xaddlem2  47008  sge0reuz  47021  sge0reuzb  47022  nnfoctbdjlem  47029  ovn0lem  47139  hoidmv1le  47168  hoidmvlelem1  47169  incsmflem  47315  decsmflem  47340  sigarcol  47438  7gbow  48394  0aryfvalel  49256  iscnrm3rlem2  49562