Theorem rspceeqv 3632

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

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1539   ∈ wcel 2104  ∃wrex 3068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ral 3060  df-rex 3069

This theorem is referenced by:  elrnmpt1s  5955  foco2  7109  fcofo  7288  onuninsuci  7831  fo1st  7997  fo2nd  7998  onnseq  8346  nneob  8657  ecelqsg  8768  resixpfo  8932  elixpsn  8933  ixpsnf1o  8934  pwfilem  9179  fofinf1o  9329  pwfilemOLD  9348  elfir  9412  inelfi  9415  fiin  9419  djur  9916  cardalephex  10087  fin23lem38  10346  fin1a2lem11  10407  fin1a2lem13  10409  reclem3pr  11046  infm3lem  12176  ccats1pfxeqrex  14669  2cshwcshw  14780  cshwcshid  14782  cshwcsh2id  14783  shftlem  15019  shftfval  15021  isercoll2  15619  infcvgaux2i  15808  mertenslem1  15834  mertenslem2  15835  fprodser  15897  bezoutlem1  16485  pcprmpw  16820  1arithlem4  16863  vdwapun  16911  vdwlem1  16918  vdwlem2  16919  vdwlem6  16923  vdwlem8  16925  elrestr  17378  gsumwspan  18763  orbsta  19218  psgneldm2i  19414  odf1o2  19482  slwhash  19533  fislw  19534  lsmelvalm  19560  pj1id  19608  efgrelexlemb  19659  cyggeninv  19792  0cyg  19802  eldprdi  19929  lss1d  20718  lspsn  20757  pwssplit1  20814  lspsneq  20880  lspprat  20911  lpi0  21085  lpi1  21086  zringcyg  21240  znf1o  21326  cygznlem3  21344  frgpcyg  21348  islindf4  21612  clsval2  22774  restcld  22896  restcldi  22897  restopnb  22899  restcls  22905  ordtbas2  22915  ordtopn1  22918  ordtopn2  22919  leordtval2  22936  iocpnfordt  22939  icomnfordt  22940  lecldbas  22943  pnrmopn  23067  cncmp  23116  fincmp  23117  cmpsublem  23123  cmpsub  23124  tgcmp  23125  uncmp  23127  cmpfi  23132  connsubclo  23148  2ndcomap  23182  dis2ndc  23184  cldllycmp  23219  dissnlocfin  23253  comppfsc  23256  ptpjopn  23336  txcmplem2  23366  qtopeu  23440  fbasrn  23608  elfm  23671  elfm3  23674  rnelfmlem  23676  rnelfm  23677  fmfnfmlem3  23680  fmfnfmlem4  23681  alexsubALTlem3  23773  ptcmplem2  23777  ptcmplem3  23778  ptcmplem5  23780  tsmsfbas  23852  trust  23954  restutopopn  23963  ustuqtop1  23966  ustuqtop2  23967  ustuqtop4  23969  ustuqtop5  23970  utopsnneiplem  23972  utopsnnei  23974  fmucnd  24017  neipcfilu  24021  mopnex  24248  metrest  24253  metustexhalf  24285  metustfbas  24286  cfilucfil  24288  restmetu  24299  metucn  24300  icoopnst  24683  iocopnst  24684  cnheibor  24701  minveclem2  25174  uniioombllem3  25334  itg1addlem4  25448  itg1addlem4OLD  25449  i1fmulc  25453  ply1lpir  25931  aannenlem2  26078  aalioulem2  26082  eflogeq  26346  cxpeq  26501  angpieqvd  26572  rlimcnp  26706  isppw2  26855  dvdsmulf1o  26934  lgsquadlem1  27119  2sqlem2  27157  mul2sq  27158  2sqlem3  27159  2sqlem9  27166  2sqlem10  27167  ostth2  27376  ostth3  27377  bdayfo  27416  scutfo  27635  addsproplem4  27694  addsproplem5  27695  addsproplem6  27696  addsfo  27705  elons2  27924  midexlem  28210  midex  28255  ttgcontlem1  28409  axcontlem7  28495  upgrex  28619  erclwwlkref  29540  clwwlkfo  29570  erclwwlknref  29589  isgrpo  30017  grpoinvf  30052  minvecolem2  30395  shsel3  30835  pjhthlem2  30912  h1de2ctlem  31075  spansncol  31088  superpos  31874  cdj3lem2  31955  wrdsplex  32371  archiabllem1a  32607  archiabllem1b  32608  cmpcref  33128  ordtconnlem1  33202  gsumesum  33355  esumcst  33359  esumpcvgval  33374  sxbrsigalem2  33583  oms0  33594  omssubadd  33597  eulerpartlemt  33668  cvmsss2  34563  cvmfolem  34568  fobigcup  35176  opnregcld  35518  cldregopn  35519  onsucsuccmpi  35631  finixpnum  36776  poimirlem16  36807  poimirlem19  36810  itg2addnclem2  36843  isbnd2  36954  isbnd3  36955  totbndbnd  36960  heibor1lem  36980  heibor  36992  rngmgmbs4  37102  prnc  37238  prtlem11  38039  lsatlspsn2  38165  lsatlspsn  38166  lfl1dim  38294  lfl1dim2N  38295  lkrss2N  38342  glbconN  38550  glbconNOLD  38551  atpointN  38917  ispsubcl2N  39121  dihglblem2aN  40467  dihglblem2N  40468  dihatexv  40512  dvh4dimat  40612  dochfl1  40650  lcfl8  40676  lcfrlem9  40724  mapdval2N  40804  mapdval4N  40806  mapdcv  40834  mapdspex  40842  hdmap14lem2a  41041  hdmap14lem6  41047  elrfi  41734  eldioph  41798  eldioph2b  41803  eldioph3  41806  eldioph4i  41852  rencldnfilem  41860  pellfund14  41938  rmxyelqirr  41950  rmxyelqirrOLD  41951  filnm  42134  unxpwdom3  42139  lpirlnr  42161  hbt  42174  rngunsnply  42217  ofoafo  42408  naddcnffo  42416  oaun3lem1  42426  dvconstbi  43395  elrestd  44098  wessf1ornlem  44182  iccshift  44529  iooshift  44533  limcperiod  44642  sumnnodd  44644  dvnprodlem1  44960  itgperiod  44995  stirlinglem13  45100  sge0rnn0  45382  sge00  45390  fsumlesge0  45391  sge0tsms  45394  sge0cl  45395  sge0f1o  45396  sge0sup  45405  sge0resplit  45420  sge0xaddlem2  45448  sge0reuz  45461  sge0reuzb  45462  nnfoctbdjlem  45469  ovn0lem  45579  hoidmv1le  45608  hoidmvlelem1  45609  incsmflem  45755  decsmflem  45780  sigarcol  45878  7gbow  46738  0aryfvalel  47407  iscnrm3rlem2  47661