Theorem preq12d 4584

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 4578	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → {𝐴, 𝐶} = {𝐵, 𝐷})
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → {𝐴, 𝐶} = {𝐵, 𝐷})

Syntax hints:   → wi 4   = wceq 1522  {cpr 4474

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-v 3439  df-un 3864  df-sn 4473  df-pr 4475

This theorem is referenced by:  opeq1  4710  csbopg  4728  opthhausdorff  5298  opthhausdorff0  5299  f1oprswap  6526  wunex2  10006  wuncval2  10015  s4prop  14108  wrdlen2  14142  wwlktovf  14154  wwlktovf1  14155  wwlktovfo  14156  wrd2f1tovbij  14158  prdsval  16557  xpsfval  16668  xpsval  16672  ipoval  17593  frmdval  17827  symg2bas  18257  xpstopnlem2  22103  tusval  22558  tmsval  22774  tmsxpsval  22831  uniiccdif  23862  dchrval  25492  eengv  26448  wkslem1  27072  wkslem2  27073  iswlk  27075  wlkonl1iedg  27129  2wlklem  27131  redwlk  27139  wlkp1lem7  27146  wlkdlem2  27150  upgrwlkdvdelem  27204  usgr2pthlem  27231  usgr2pth  27232  crctcshwlkn0lem4  27278  crctcshwlkn0lem5  27279  crctcshwlkn0lem6  27280  iswwlks  27301  0enwwlksnge1  27329  wlkiswwlks2lem2  27335  wlkiswwlks2lem5  27338  wwlksm1edg  27346  wwlksnred  27357  wwlksnext  27358  wwlksnredwwlkn  27360  wwlksnextproplem2  27376  2wlkdlem10  27401  umgrwwlks2on  27423  rusgrnumwwlkl1  27434  isclwwlk  27449  clwwlkccatlem  27454  clwwlkccat  27455  clwlkclwwlklem2a1  27457  clwlkclwwlklem2fv1  27460  clwlkclwwlklem2a4  27462  clwlkclwwlklem2a  27463  clwlkclwwlklem2  27465  clwlkclwwlk  27467  clwwisshclwwslemlem  27478  clwwisshclwwslem  27479  clwwisshclwws  27480  clwwlkinwwlk  27505  clwwlkn2  27509  clwwlkel  27512  clwwlkf  27513  clwwlkwwlksb  27520  clwwlkext2edg  27522  wwlksext2clwwlk  27523  wwlksubclwwlk  27524  umgr2cwwk2dif  27530  s2elclwwlknon2  27570  clwwlknonex2lem2  27574  clwwlknonex2  27575  3wlkdlem10  27635  upgr3v3e3cycl  27646  upgr4cycl4dv4e  27651  eupthseg  27672  upgreupthseg  27675  eupth2lem3  27703  nfrgr2v  27743  frgr3vlem1  27744  frgr3vlem2  27745  4cycl2vnunb  27761  disjdifprg  30015  s2rn  30300  kur14lem1  32061  kur14  32071  tgrpfset  37411  tgrpset  37412  hlhilset  38601  dfac21  39151  mendval  39268  mnurndlem1  40114  sge0sn  42203  isomuspgrlem2b  43476  isupwlk  43493  zlmodzxzsub  43886  prelrrx2b  44182  rrx2plordisom  44191  onsetreclem1  44287