Theorem rspceeqv 3611

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∃wrex 3053

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054

This theorem is referenced by:  elrnmpt1s  5923  foco2  7081  fcofo  7263  onuninsuci  7816  fo1st  7988  fo2nd  7989  onnseq  8313  nneob  8620  ecelqs  8741  resixpfo  8909  elixpsn  8910  ixpsnf1o  8911  pwfilem  9267  fofinf1o  9283  elfir  9366  inelfi  9369  fiin  9373  djur  9872  cardalephex  10043  fin23lem38  10302  fin1a2lem11  10363  fin1a2lem13  10365  reclem3pr  11002  infm3lem  12141  ccats1pfxeqrex  14680  2cshwcshw  14791  cshwcshid  14793  cshwcsh2id  14794  shftlem  15034  shftfval  15036  isercoll2  15635  infcvgaux2i  15824  mertenslem1  15850  mertenslem2  15851  fprodser  15915  bezoutlem1  16509  pcprmpw  16854  1arithlem4  16897  vdwapun  16945  vdwlem1  16952  vdwlem2  16953  vdwlem6  16957  vdwlem8  16959  elrestr  17391  gsumwspan  18773  orbsta  19245  psgneldm2i  19435  odf1o2  19503  slwhash  19554  fislw  19555  lsmelvalm  19581  pj1id  19629  efgrelexlemb  19680  cyggeninv  19813  0cyg  19823  eldprdi  19950  lss1d  20869  lspsn  20908  pwssplit1  20966  lspsneq  21032  lspprat  21063  lpi0  21236  lpi1  21237  zringcyg  21379  znf1o  21461  cygznlem3  21479  frgpcyg  21483  islindf4  21747  clsval2  22937  restcld  23059  restcldi  23060  restopnb  23062  restcls  23068  ordtbas2  23078  ordtopn1  23081  ordtopn2  23082  leordtval2  23099  iocpnfordt  23102  icomnfordt  23103  lecldbas  23106  pnrmopn  23230  cncmp  23279  fincmp  23280  cmpsublem  23286  cmpsub  23287  tgcmp  23288  uncmp  23290  cmpfi  23295  connsubclo  23311  2ndcomap  23345  dis2ndc  23347  cldllycmp  23382  dissnlocfin  23416  comppfsc  23419  ptpjopn  23499  txcmplem2  23529  qtopeu  23603  fbasrn  23771  elfm  23834  elfm3  23837  rnelfmlem  23839  rnelfm  23840  fmfnfmlem3  23843  fmfnfmlem4  23844  alexsubALTlem3  23936  ptcmplem2  23940  ptcmplem3  23941  ptcmplem5  23943  tsmsfbas  24015  trust  24117  restutopopn  24126  ustuqtop1  24129  ustuqtop2  24130  ustuqtop4  24132  ustuqtop5  24133  utopsnneiplem  24135  utopsnnei  24137  fmucnd  24179  neipcfilu  24183  mopnex  24407  metrest  24412  metustexhalf  24444  metustfbas  24445  cfilucfil  24447  restmetu  24458  metucn  24459  icoopnst  24836  iocopnst  24837  cnheibor  24854  minveclem2  25326  uniioombllem3  25486  itg1addlem4  25600  i1fmulc  25604  ply1lpir  26087  aannenlem2  26237  aalioulem2  26241  eflogeq  26511  cxpeq  26667  angpieqvd  26741  rlimcnp  26875  isppw2  27025  mpodvdsmulf1o  27104  dvdsmulf1o  27106  lgsquadlem1  27291  2sqlem2  27329  mul2sq  27330  2sqlem3  27331  2sqlem9  27338  2sqlem10  27339  ostth2  27548  ostth3  27549  bdayfo  27589  scutfo  27816  addsproplem4  27879  addsproplem5  27880  addsproplem6  27881  addsfo  27890  subsfo  27969  elons2  28159  n0seo  28307  zseo  28308  midexlem  28619  midex  28664  ttgcontlem1  28812  axcontlem7  28897  upgrex  29019  erclwwlkref  29949  clwwlkfo  29979  erclwwlknref  29998  isgrpo  30426  grpoinvf  30461  minvecolem2  30804  shsel3  31244  pjhthlem2  31321  h1de2ctlem  31484  spansncol  31497  superpos  32283  cdj3lem2  32364  wrdsplex  32857  archiabllem1a  33145  archiabllem1b  33146  cmpcref  33840  ordtconnlem1  33914  gsumesum  34049  esumcst  34053  esumpcvgval  34068  sxbrsigalem2  34277  oms0  34288  omssubadd  34291  eulerpartlemt  34362  cvmsss2  35261  cvmfolem  35266  fobigcup  35888  opnregcld  36318  cldregopn  36319  onsucsuccmpi  36431  finixpnum  37599  poimirlem16  37630  poimirlem19  37633  itg2addnclem2  37666  isbnd2  37777  isbnd3  37778  totbndbnd  37783  heibor1lem  37803  heibor  37815  rngmgmbs4  37925  prnc  38061  prtlem11  38859  lsatlspsn2  38985  lsatlspsn  38986  lfl1dim  39114  lfl1dim2N  39115  lkrss2N  39162  glbconN  39370  glbconNOLD  39371  atpointN  39737  ispsubcl2N  39941  dihglblem2aN  41287  dihglblem2N  41288  dihatexv  41332  dvh4dimat  41432  dochfl1  41470  lcfl8  41496  lcfrlem9  41544  mapdval2N  41624  mapdval4N  41626  mapdcv  41654  mapdspex  41662  hdmap14lem2a  41861  hdmap14lem6  41867  elrfi  42682  eldioph  42746  eldioph2b  42751  eldioph3  42754  eldioph4i  42800  rencldnfilem  42808  pellfund14  42886  rmxyelqirr  42898  rmxyelqirrOLD  42899  filnm  43079  unxpwdom3  43084  lpirlnr  43106  hbt  43119  rngunsnply  43158  ofoafo  43345  naddcnffo  43353  oaun3lem1  43363  dvconstbi  44323  elrestd  45102  wessf1ornlem  45179  iccshift  45516  iooshift  45520  limcperiod  45626  sumnnodd  45628  dvnprodlem1  45944  itgperiod  45979  stirlinglem13  46084  sge0rnn0  46366  sge00  46374  fsumlesge0  46375  sge0tsms  46378  sge0cl  46379  sge0f1o  46380  sge0sup  46389  sge0resplit  46404  sge0xaddlem2  46432  sge0reuz  46445  sge0reuzb  46446  nnfoctbdjlem  46453  ovn0lem  46563  hoidmv1le  46592  hoidmvlelem1  46593  incsmflem  46739  decsmflem  46764  sigarcol  46862  7gbow  47773  0aryfvalel  48623  iscnrm3rlem2  48929