Theorem rspceeqv 3577

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1522   ∈ wcel 2081  ∃wrex 3106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-rex 3111  df-v 3439

This theorem is referenced by:  elrnmpt1s  5711  foco2  6736  fcofo  6909  onuninsuci  7411  fo1st  7565  fo2nd  7566  onnseq  7833  nneob  8129  ecelqsg  8202  resixpfo  8348  elixpsn  8349  ixpsnf1o  8350  fofinf1o  8645  pwfilem  8664  elfir  8725  inelfi  8728  fiin  8732  djur  9194  cardalephex  9362  fin23lem38  9617  fin1a2lem11  9678  fin1a2lem13  9680  reclem3pr  10317  infm3lem  11447  zqOLD  12204  ccats1pfxeqrex  13913  2cshwcshw  14023  cshwcshid  14025  cshwcsh2id  14026  shftlem  14261  shftfval  14263  isercoll2  14859  infcvgaux2i  15046  mertenslem1  15073  mertenslem2  15074  fprodser  15136  bezoutlem1  15716  pcprmpw  16048  1arithlem4  16091  vdwapun  16139  vdwlem1  16146  vdwlem2  16147  vdwlem6  16151  vdwlem8  16153  elrestr  16531  gsumwspan  17822  orbsta  18184  psgneldm2i  18364  odf1o2  18428  slwhash  18479  fislw  18480  lsmelvalm  18506  pj1id  18552  efgrelexlemb  18603  cyggeninv  18725  0cyg  18734  eldprdi  18857  lss1d  19425  lspsn  19464  pwssplit1  19521  lspsneq  19584  lspprat  19615  lpi0  19709  lpi1  19710  zringcyg  20320  znf1o  20380  cygznlem3  20398  frgpcyg  20402  islindf4  20664  clsval2  21342  restcld  21464  restcldi  21465  restopnb  21467  restcls  21473  ordtbas2  21483  ordtopn1  21486  ordtopn2  21487  leordtval2  21504  iocpnfordt  21507  icomnfordt  21508  lecldbas  21511  pnrmopn  21635  cncmp  21684  fincmp  21685  cmpsublem  21691  cmpsub  21692  tgcmp  21693  uncmp  21695  cmpfi  21700  connsubclo  21716  2ndcomap  21750  dis2ndc  21752  cldllycmp  21787  dissnlocfin  21821  comppfsc  21824  ptpjopn  21904  txcmplem2  21934  qtopeu  22008  fbasrn  22176  elfm  22239  elfm3  22242  rnelfmlem  22244  rnelfm  22245  fmfnfmlem3  22248  fmfnfmlem4  22249  alexsubALTlem3  22341  ptcmplem2  22345  ptcmplem3  22346  ptcmplem5  22348  tsmsfbas  22419  trust  22521  restutopopn  22530  ustuqtop1  22533  ustuqtop2  22534  ustuqtop4  22536  ustuqtop5  22537  utopsnneiplem  22539  utopsnnei  22541  fmucnd  22584  neipcfilu  22588  mopnex  22812  metrest  22817  metustexhalf  22849  metustfbas  22850  cfilucfil  22852  restmetu  22863  metucn  22864  icoopnst  23226  iocopnst  23227  cnheibor  23242  minveclem2  23712  uniioombllem3  23869  itg1addlem4  23983  i1fmulc  23987  ply1lpir  24455  aannenlem2  24601  aalioulem2  24605  eflogeq  24866  cxpeq  25019  angpieqvd  25090  rlimcnp  25225  isppw2  25374  dvdsmulf1o  25453  lgsquadlem1  25638  2sqlem2  25676  mul2sq  25677  2sqlem3  25678  2sqlem9  25685  2sqlem10  25686  ostth2  25895  ostth3  25896  midexlem  26160  midex  26205  ttgcontlem1  26354  axcontlem7  26439  upgrex  26560  erclwwlkref  27485  clwwlkfo  27516  erclwwlknref  27535  isgrpo  27965  grpoinvf  28000  minvecolem2  28343  shsel3  28783  pjhthlem2  28860  h1de2ctlem  29023  spansncol  29036  superpos  29822  cdj3lem2  29903  wrdsplex  30298  archiabllem1a  30458  archiabllem1b  30459  cmpcref  30731  ordtconnlem1  30784  gsumesum  30935  esumcst  30939  esumpcvgval  30954  sxbrsigalem2  31161  oms0  31172  omssubadd  31175  eulerpartlemt  31246  cvmsss2  32129  cvmfolem  32134  bdayfo  32791  fobigcup  32970  opnregcld  33287  cldregopn  33288  onsucsuccmpi  33400  finixpnum  34408  poimirlem16  34439  poimirlem19  34442  itg2addnclem2  34475  isbnd2  34593  isbnd3  34594  totbndbnd  34599  heibor1lem  34619  heibor  34631  rngmgmbs4  34741  prnc  34877  prtlem11  35533  lsatlspsn2  35659  lsatlspsn  35660  lfl1dim  35788  lfl1dim2N  35789  lkrss2N  35836  glbconN  36044  atpointN  36410  ispsubcl2N  36614  dihglblem2aN  37960  dihglblem2N  37961  dihatexv  38005  dvh4dimat  38105  dochfl1  38143  lcfl8  38169  lcfrlem9  38217  mapdval2N  38297  mapdval4N  38299  mapdcv  38327  mapdspex  38335  hdmap14lem2a  38534  hdmap14lem6  38540  elrfi  38776  eldioph  38840  eldioph2b  38845  eldioph3  38848  eldioph4i  38894  rencldnfilem  38902  pellfund14  38980  rmxyelqirr  38992  filnm  39175  unxpwdom3  39180  lpirlnr  39202  hbt  39215  rngunsnply  39258  dvconstbi  40204  elrestd  40914  wessf1ornlem  40985  iccshift  41336  iooshift  41340  limcperiod  41451  sumnnodd  41453  dvnprodlem1  41772  itgperiod  41807  stirlinglem13  41913  sge0rnn0  42192  sge00  42200  fsumlesge0  42201  sge0tsms  42204  sge0cl  42205  sge0f1o  42206  sge0sup  42215  sge0resplit  42230  sge0xaddlem2  42258  sge0reuz  42271  sge0reuzb  42272  nnfoctbdjlem  42279  ovn0lem  42389  hoidmv1le  42418  hoidmvlelem1  42419  incsmflem  42560  decsmflem  42584  sigarcol  42663  7gbow  43419