Theorem rspceeqv 3614

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 3591	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐸 = 𝐷) → ∃𝑥 ∈ 𝐵 𝐸 = 𝐶)

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055

This theorem is referenced by:  elrnmpt1s  5926  foco2  7084  fcofo  7266  onuninsuci  7819  fo1st  7991  fo2nd  7992  onnseq  8316  nneob  8623  ecelqs  8744  resixpfo  8912  elixpsn  8913  ixpsnf1o  8914  pwfilem  9274  fofinf1o  9290  elfir  9373  inelfi  9376  fiin  9380  djur  9879  cardalephex  10050  fin23lem38  10309  fin1a2lem11  10370  fin1a2lem13  10372  reclem3pr  11009  infm3lem  12148  ccats1pfxeqrex  14687  2cshwcshw  14798  cshwcshid  14800  cshwcsh2id  14801  shftlem  15041  shftfval  15043  isercoll2  15642  infcvgaux2i  15831  mertenslem1  15857  mertenslem2  15858  fprodser  15922  bezoutlem1  16516  pcprmpw  16861  1arithlem4  16904  vdwapun  16952  vdwlem1  16959  vdwlem2  16960  vdwlem6  16964  vdwlem8  16966  elrestr  17398  gsumwspan  18780  orbsta  19252  psgneldm2i  19442  odf1o2  19510  slwhash  19561  fislw  19562  lsmelvalm  19588  pj1id  19636  efgrelexlemb  19687  cyggeninv  19820  0cyg  19830  eldprdi  19957  lss1d  20876  lspsn  20915  pwssplit1  20973  lspsneq  21039  lspprat  21070  lpi0  21243  lpi1  21244  zringcyg  21386  znf1o  21468  cygznlem3  21486  frgpcyg  21490  islindf4  21754  clsval2  22944  restcld  23066  restcldi  23067  restopnb  23069  restcls  23075  ordtbas2  23085  ordtopn1  23088  ordtopn2  23089  leordtval2  23106  iocpnfordt  23109  icomnfordt  23110  lecldbas  23113  pnrmopn  23237  cncmp  23286  fincmp  23287  cmpsublem  23293  cmpsub  23294  tgcmp  23295  uncmp  23297  cmpfi  23302  connsubclo  23318  2ndcomap  23352  dis2ndc  23354  cldllycmp  23389  dissnlocfin  23423  comppfsc  23426  ptpjopn  23506  txcmplem2  23536  qtopeu  23610  fbasrn  23778  elfm  23841  elfm3  23844  rnelfmlem  23846  rnelfm  23847  fmfnfmlem3  23850  fmfnfmlem4  23851  alexsubALTlem3  23943  ptcmplem2  23947  ptcmplem3  23948  ptcmplem5  23950  tsmsfbas  24022  trust  24124  restutopopn  24133  ustuqtop1  24136  ustuqtop2  24137  ustuqtop4  24139  ustuqtop5  24140  utopsnneiplem  24142  utopsnnei  24144  fmucnd  24186  neipcfilu  24190  mopnex  24414  metrest  24419  metustexhalf  24451  metustfbas  24452  cfilucfil  24454  restmetu  24465  metucn  24466  icoopnst  24843  iocopnst  24844  cnheibor  24861  minveclem2  25333  uniioombllem3  25493  itg1addlem4  25607  i1fmulc  25611  ply1lpir  26094  aannenlem2  26244  aalioulem2  26248  eflogeq  26518  cxpeq  26674  angpieqvd  26748  rlimcnp  26882  isppw2  27032  mpodvdsmulf1o  27111  dvdsmulf1o  27113  lgsquadlem1  27298  2sqlem2  27336  mul2sq  27337  2sqlem3  27338  2sqlem9  27345  2sqlem10  27346  ostth2  27555  ostth3  27556  bdayfo  27596  scutfo  27823  addsproplem4  27886  addsproplem5  27887  addsproplem6  27888  addsfo  27897  subsfo  27976  elons2  28166  n0seo  28314  zseo  28315  midexlem  28626  midex  28671  ttgcontlem1  28819  axcontlem7  28904  upgrex  29026  erclwwlkref  29956  clwwlkfo  29986  erclwwlknref  30005  isgrpo  30433  grpoinvf  30468  minvecolem2  30811  shsel3  31251  pjhthlem2  31328  h1de2ctlem  31491  spansncol  31504  superpos  32290  cdj3lem2  32371  wrdsplex  32864  archiabllem1a  33152  archiabllem1b  33153  cmpcref  33847  ordtconnlem1  33921  gsumesum  34056  esumcst  34060  esumpcvgval  34075  sxbrsigalem2  34284  oms0  34295  omssubadd  34298  eulerpartlemt  34369  cvmsss2  35268  cvmfolem  35273  fobigcup  35895  opnregcld  36325  cldregopn  36326  onsucsuccmpi  36438  finixpnum  37606  poimirlem16  37637  poimirlem19  37640  itg2addnclem2  37673  isbnd2  37784  isbnd3  37785  totbndbnd  37790  heibor1lem  37810  heibor  37822  rngmgmbs4  37932  prnc  38068  prtlem11  38866  lsatlspsn2  38992  lsatlspsn  38993  lfl1dim  39121  lfl1dim2N  39122  lkrss2N  39169  glbconN  39377  glbconNOLD  39378  atpointN  39744  ispsubcl2N  39948  dihglblem2aN  41294  dihglblem2N  41295  dihatexv  41339  dvh4dimat  41439  dochfl1  41477  lcfl8  41503  lcfrlem9  41551  mapdval2N  41631  mapdval4N  41633  mapdcv  41661  mapdspex  41669  hdmap14lem2a  41868  hdmap14lem6  41874  elrfi  42689  eldioph  42753  eldioph2b  42758  eldioph3  42761  eldioph4i  42807  rencldnfilem  42815  pellfund14  42893  rmxyelqirr  42905  rmxyelqirrOLD  42906  filnm  43086  unxpwdom3  43091  lpirlnr  43113  hbt  43126  rngunsnply  43165  ofoafo  43352  naddcnffo  43360  oaun3lem1  43370  dvconstbi  44330  elrestd  45109  wessf1ornlem  45186  iccshift  45523  iooshift  45527  limcperiod  45633  sumnnodd  45635  dvnprodlem1  45951  itgperiod  45986  stirlinglem13  46091  sge0rnn0  46373  sge00  46381  fsumlesge0  46382  sge0tsms  46385  sge0cl  46386  sge0f1o  46387  sge0sup  46396  sge0resplit  46411  sge0xaddlem2  46439  sge0reuz  46452  sge0reuzb  46453  nnfoctbdjlem  46460  ovn0lem  46570  hoidmv1le  46599  hoidmvlelem1  46600  incsmflem  46746  decsmflem  46771  sigarcol  46869  7gbow  47777  0aryfvalel  48627  iscnrm3rlem2  48933