Theorem preq12d 4643

Description: Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)

Hypotheses

Ref	Expression
preq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)
preq12d.2	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
preq12d	⊢ (𝜑 → {𝐴, 𝐶} = {𝐵, 𝐷})

Proof of Theorem preq12d

Step	Hyp	Ref	Expression
1		preq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		preq12d.2	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
3		preq12 4637	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → {𝐴, 𝐶} = {𝐵, 𝐷})
4	1, 2, 3	syl2anc 587	1 ⊢ (𝜑 → {𝐴, 𝐶} = {𝐵, 𝐷})

Syntax hints:   → wi 4   = wceq 1543  {cpr 4529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-un 3858  df-sn 4528  df-pr 4530

This theorem is referenced by:  opeq1  4770  csbopg  4788  opthhausdorff  5385  opthhausdorff0  5386  f1oprswap  6682  wunex2  10317  wuncval2  10326  s4prop  14440  wrdlen2  14474  wwlktovf  14488  wwlktovf1  14489  wwlktovfo  14490  wrd2f1tovbij  14492  prdsval  16914  xpsfval  17025  xpsval  17029  ipoval  17990  frmdval  18232  symg2bas  18739  xpstopnlem2  22662  tusval  23117  tmsval  23333  tmsxpsval  23390  uniiccdif  24429  dchrval  26069  eengv  27024  wkslem1  27649  wkslem2  27650  iswlk  27652  wlkonl1iedg  27707  2wlklem  27709  redwlk  27714  wlkp1lem7  27721  wlkdlem2  27725  upgrwlkdvdelem  27777  usgr2pthlem  27804  usgr2pth  27805  crctcshwlkn0lem4  27851  crctcshwlkn0lem5  27852  crctcshwlkn0lem6  27853  iswwlks  27874  0enwwlksnge1  27902  wlkiswwlks2lem2  27908  wlkiswwlks2lem5  27911  wwlksm1edg  27919  wwlksnred  27930  wwlksnext  27931  wwlksnredwwlkn  27933  wwlksnextproplem2  27948  2wlkdlem10  27973  umgrwwlks2on  27995  rusgrnumwwlkl1  28006  isclwwlk  28021  clwwlkccatlem  28026  clwwlkccat  28027  clwlkclwwlklem2a1  28029  clwlkclwwlklem2fv1  28032  clwlkclwwlklem2a4  28034  clwlkclwwlklem2a  28035  clwlkclwwlklem2  28037  clwlkclwwlk  28039  clwwisshclwwslemlem  28050  clwwisshclwwslem  28051  clwwisshclwws  28052  clwwlkinwwlk  28077  clwwlkn2  28081  clwwlkel  28083  clwwlkf  28084  clwwlkwwlksb  28091  clwwlkext2edg  28093  wwlksext2clwwlk  28094  wwlksubclwwlk  28095  umgr2cwwk2dif  28101  s2elclwwlknon2  28141  clwwlknonex2lem2  28145  clwwlknonex2  28146  3wlkdlem10  28206  upgr3v3e3cycl  28217  upgr4cycl4dv4e  28222  eupthseg  28243  upgreupthseg  28246  eupth2lem3  28273  nfrgr2v  28309  frgr3vlem1  28310  frgr3vlem2  28311  4cycl2vnunb  28327  disjdifprg  30587  s2rn  30892  idlsrgval  31316  revwlk  32753  kur14lem1  32835  kur14  32845  bj-endval  35169  tgrpfset  38444  tgrpset  38445  hlhilset  39634  dfac21  40535  mendval  40652  mnurndlem1  41513  sge0sn  43535  isomuspgrlem2b  44897  isupwlk  44914  zlmodzxzsub  45312  2arymaptf  45614  prelrrx2b  45676  rrx2plordisom  45685  onsetreclem1  46024