Theorem rspceeqv 3567

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2108  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069

This theorem is referenced by:  elrnmpt1s  5855  foco2  6965  fcofo  7140  onuninsuci  7662  fo1st  7824  fo2nd  7825  onnseq  8146  nneob  8446  ecelqsg  8519  resixpfo  8682  elixpsn  8683  ixpsnf1o  8684  pwfilem  8922  fofinf1o  9024  pwfilemOLD  9043  elfir  9104  inelfi  9107  fiin  9111  djur  9608  cardalephex  9777  fin23lem38  10036  fin1a2lem11  10097  fin1a2lem13  10099  reclem3pr  10736  infm3lem  11863  ccats1pfxeqrex  14356  2cshwcshw  14466  cshwcshid  14468  cshwcsh2id  14469  shftlem  14707  shftfval  14709  isercoll2  15308  infcvgaux2i  15498  mertenslem1  15524  mertenslem2  15525  fprodser  15587  bezoutlem1  16175  pcprmpw  16512  1arithlem4  16555  vdwapun  16603  vdwlem1  16610  vdwlem2  16611  vdwlem6  16615  vdwlem8  16617  elrestr  17056  gsumwspan  18400  orbsta  18834  psgneldm2i  19028  odf1o2  19093  slwhash  19144  fislw  19145  lsmelvalm  19171  pj1id  19220  efgrelexlemb  19271  cyggeninv  19398  0cyg  19409  eldprdi  19536  lss1d  20140  lspsn  20179  pwssplit1  20236  lspsneq  20299  lspprat  20330  lpi0  20431  lpi1  20432  zringcyg  20603  znf1o  20671  cygznlem3  20689  frgpcyg  20693  islindf4  20955  clsval2  22109  restcld  22231  restcldi  22232  restopnb  22234  restcls  22240  ordtbas2  22250  ordtopn1  22253  ordtopn2  22254  leordtval2  22271  iocpnfordt  22274  icomnfordt  22275  lecldbas  22278  pnrmopn  22402  cncmp  22451  fincmp  22452  cmpsublem  22458  cmpsub  22459  tgcmp  22460  uncmp  22462  cmpfi  22467  connsubclo  22483  2ndcomap  22517  dis2ndc  22519  cldllycmp  22554  dissnlocfin  22588  comppfsc  22591  ptpjopn  22671  txcmplem2  22701  qtopeu  22775  fbasrn  22943  elfm  23006  elfm3  23009  rnelfmlem  23011  rnelfm  23012  fmfnfmlem3  23015  fmfnfmlem4  23016  alexsubALTlem3  23108  ptcmplem2  23112  ptcmplem3  23113  ptcmplem5  23115  tsmsfbas  23187  trust  23289  restutopopn  23298  ustuqtop1  23301  ustuqtop2  23302  ustuqtop4  23304  ustuqtop5  23305  utopsnneiplem  23307  utopsnnei  23309  fmucnd  23352  neipcfilu  23356  mopnex  23581  metrest  23586  metustexhalf  23618  metustfbas  23619  cfilucfil  23621  restmetu  23632  metucn  23633  icoopnst  24008  iocopnst  24009  cnheibor  24024  minveclem2  24495  uniioombllem3  24654  itg1addlem4  24768  itg1addlem4OLD  24769  i1fmulc  24773  ply1lpir  25248  aannenlem2  25394  aalioulem2  25398  eflogeq  25662  cxpeq  25815  angpieqvd  25886  rlimcnp  26020  isppw2  26169  dvdsmulf1o  26248  lgsquadlem1  26433  2sqlem2  26471  mul2sq  26472  2sqlem3  26473  2sqlem9  26480  2sqlem10  26481  ostth2  26690  ostth3  26691  midexlem  26957  midex  27002  ttgcontlem1  27155  axcontlem7  27241  upgrex  27365  erclwwlkref  28285  clwwlkfo  28315  erclwwlknref  28334  isgrpo  28760  grpoinvf  28795  minvecolem2  29138  shsel3  29578  pjhthlem2  29655  h1de2ctlem  29818  spansncol  29831  superpos  30617  cdj3lem2  30698  wrdsplex  31114  archiabllem1a  31347  archiabllem1b  31348  cmpcref  31702  ordtconnlem1  31776  gsumesum  31927  esumcst  31931  esumpcvgval  31946  sxbrsigalem2  32153  oms0  32164  omssubadd  32167  eulerpartlemt  32238  cvmsss2  33136  cvmfolem  33141  bdayfo  33807  scutfo  34011  fobigcup  34129  opnregcld  34446  cldregopn  34447  onsucsuccmpi  34559  finixpnum  35689  poimirlem16  35720  poimirlem19  35723  itg2addnclem2  35756  isbnd2  35868  isbnd3  35869  totbndbnd  35874  heibor1lem  35894  heibor  35906  rngmgmbs4  36016  prnc  36152  prtlem11  36807  lsatlspsn2  36933  lsatlspsn  36934  lfl1dim  37062  lfl1dim2N  37063  lkrss2N  37110  glbconN  37318  atpointN  37684  ispsubcl2N  37888  dihglblem2aN  39234  dihglblem2N  39235  dihatexv  39279  dvh4dimat  39379  dochfl1  39417  lcfl8  39443  lcfrlem9  39491  mapdval2N  39571  mapdval4N  39573  mapdcv  39601  mapdspex  39609  hdmap14lem2a  39808  hdmap14lem6  39814  elrfi  40432  eldioph  40496  eldioph2b  40501  eldioph3  40504  eldioph4i  40550  rencldnfilem  40558  pellfund14  40636  rmxyelqirr  40648  filnm  40831  unxpwdom3  40836  lpirlnr  40858  hbt  40871  rngunsnply  40914  dvconstbi  41841  elrestd  42547  wessf1ornlem  42611  iccshift  42946  iooshift  42950  limcperiod  43059  sumnnodd  43061  dvnprodlem1  43377  itgperiod  43412  stirlinglem13  43517  sge0rnn0  43796  sge00  43804  fsumlesge0  43805  sge0tsms  43808  sge0cl  43809  sge0f1o  43810  sge0sup  43819  sge0resplit  43834  sge0xaddlem2  43862  sge0reuz  43875  sge0reuzb  43876  nnfoctbdjlem  43883  ovn0lem  43993  hoidmv1le  44022  hoidmvlelem1  44023  incsmflem  44164  decsmflem  44188  sigarcol  44267  7gbow  45112  0aryfvalel  45868  iscnrm3rlem2  46123