Theorem rspceeqv 3608

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 3585	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  5912  foco2  7063  fcofo  7245  onuninsuci  7796  fo1st  7967  fo2nd  7968  onnseq  8290  nneob  8597  ecelqs  8718  resixpfo  8886  elixpsn  8887  ixpsnf1o  8888  pwfilem  9243  fofinf1o  9259  elfir  9342  inelfi  9345  fiin  9349  djur  9848  cardalephex  10019  fin23lem38  10278  fin1a2lem11  10339  fin1a2lem13  10341  reclem3pr  10978  infm3lem  12117  ccats1pfxeqrex  14656  2cshwcshw  14767  cshwcshid  14769  cshwcsh2id  14770  shftlem  15010  shftfval  15012  isercoll2  15611  infcvgaux2i  15800  mertenslem1  15826  mertenslem2  15827  fprodser  15891  bezoutlem1  16485  pcprmpw  16830  1arithlem4  16873  vdwapun  16921  vdwlem1  16928  vdwlem2  16929  vdwlem6  16933  vdwlem8  16935  elrestr  17367  gsumwspan  18755  orbsta  19227  psgneldm2i  19419  odf1o2  19487  slwhash  19538  fislw  19539  lsmelvalm  19565  pj1id  19613  efgrelexlemb  19664  cyggeninv  19797  0cyg  19807  eldprdi  19934  lss1d  20901  lspsn  20940  pwssplit1  20998  lspsneq  21064  lspprat  21095  lpi0  21268  lpi1  21269  zringcyg  21411  znf1o  21493  cygznlem3  21511  frgpcyg  21515  islindf4  21780  clsval2  22970  restcld  23092  restcldi  23093  restopnb  23095  restcls  23101  ordtbas2  23111  ordtopn1  23114  ordtopn2  23115  leordtval2  23132  iocpnfordt  23135  icomnfordt  23136  lecldbas  23139  pnrmopn  23263  cncmp  23312  fincmp  23313  cmpsublem  23319  cmpsub  23320  tgcmp  23321  uncmp  23323  cmpfi  23328  connsubclo  23344  2ndcomap  23378  dis2ndc  23380  cldllycmp  23415  dissnlocfin  23449  comppfsc  23452  ptpjopn  23532  txcmplem2  23562  qtopeu  23636  fbasrn  23804  elfm  23867  elfm3  23870  rnelfmlem  23872  rnelfm  23873  fmfnfmlem3  23876  fmfnfmlem4  23877  alexsubALTlem3  23969  ptcmplem2  23973  ptcmplem3  23974  ptcmplem5  23976  tsmsfbas  24048  trust  24150  restutopopn  24159  ustuqtop1  24162  ustuqtop2  24163  ustuqtop4  24165  ustuqtop5  24166  utopsnneiplem  24168  utopsnnei  24170  fmucnd  24212  neipcfilu  24216  mopnex  24440  metrest  24445  metustexhalf  24477  metustfbas  24478  cfilucfil  24480  restmetu  24491  metucn  24492  icoopnst  24869  iocopnst  24870  cnheibor  24887  minveclem2  25359  uniioombllem3  25519  itg1addlem4  25633  i1fmulc  25637  ply1lpir  26120  aannenlem2  26270  aalioulem2  26274  eflogeq  26544  cxpeq  26700  angpieqvd  26774  rlimcnp  26908  isppw2  27058  mpodvdsmulf1o  27137  dvdsmulf1o  27139  lgsquadlem1  27324  2sqlem2  27362  mul2sq  27363  2sqlem3  27364  2sqlem9  27371  2sqlem10  27372  ostth2  27581  ostth3  27582  bdayfo  27622  scutfo  27854  addsproplem4  27919  addsproplem5  27920  addsproplem6  27921  addsfo  27930  subsfo  28009  elons2  28199  n0seo  28348  zseo  28349  midexlem  28672  midex  28717  ttgcontlem1  28865  axcontlem7  28950  upgrex  29072  erclwwlkref  29999  clwwlkfo  30029  erclwwlknref  30048  isgrpo  30476  grpoinvf  30511  minvecolem2  30854  shsel3  31294  pjhthlem2  31371  h1de2ctlem  31534  spansncol  31547  superpos  32333  cdj3lem2  32414  wrdsplex  32907  archiabllem1a  33160  archiabllem1b  33161  cmpcref  33833  ordtconnlem1  33907  gsumesum  34042  esumcst  34046  esumpcvgval  34061  sxbrsigalem2  34270  oms0  34281  omssubadd  34284  eulerpartlemt  34355  cvmsss2  35254  cvmfolem  35259  fobigcup  35881  opnregcld  36311  cldregopn  36312  onsucsuccmpi  36424  finixpnum  37592  poimirlem16  37623  poimirlem19  37626  itg2addnclem2  37659  isbnd2  37770  isbnd3  37771  totbndbnd  37776  heibor1lem  37796  heibor  37808  rngmgmbs4  37918  prnc  38054  prtlem11  38852  lsatlspsn2  38978  lsatlspsn  38979  lfl1dim  39107  lfl1dim2N  39108  lkrss2N  39155  glbconN  39363  glbconNOLD  39364  atpointN  39730  ispsubcl2N  39934  dihglblem2aN  41280  dihglblem2N  41281  dihatexv  41325  dvh4dimat  41425  dochfl1  41463  lcfl8  41489  lcfrlem9  41537  mapdval2N  41617  mapdval4N  41619  mapdcv  41647  mapdspex  41655  hdmap14lem2a  41854  hdmap14lem6  41860  elrfi  42675  eldioph  42739  eldioph2b  42744  eldioph3  42747  eldioph4i  42793  rencldnfilem  42801  pellfund14  42879  rmxyelqirr  42891  rmxyelqirrOLD  42892  filnm  43072  unxpwdom3  43077  lpirlnr  43099  hbt  43112  rngunsnply  43151  ofoafo  43338  naddcnffo  43346  oaun3lem1  43356  dvconstbi  44316  elrestd  45095  wessf1ornlem  45172  iccshift  45509  iooshift  45513  limcperiod  45619  sumnnodd  45621  dvnprodlem1  45937  itgperiod  45972  stirlinglem13  46077  sge0rnn0  46359  sge00  46367  fsumlesge0  46368  sge0tsms  46371  sge0cl  46372  sge0f1o  46373  sge0sup  46382  sge0resplit  46397  sge0xaddlem2  46425  sge0reuz  46438  sge0reuzb  46439  nnfoctbdjlem  46446  ovn0lem  46556  hoidmv1le  46585  hoidmvlelem1  46586  incsmflem  46732  decsmflem  46757  sigarcol  46855  7gbow  47766  0aryfvalel  48616  iscnrm3rlem2  48922