Theorem preq12d 4663

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

Syntax hints:   → wi 4   = wceq 1537  {cpr 4555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3488  df-un 3929  df-sn 4554  df-pr 4556

This theorem is referenced by:  opeq1  4789  csbopg  4807  opthhausdorff  5393  opthhausdorff0  5394  f1oprswap  6644  wunex2  10146  wuncval2  10155  s4prop  14257  wrdlen2  14291  wwlktovf  14305  wwlktovf1  14306  wwlktovfo  14307  wrd2f1tovbij  14309  prdsval  16711  xpsfval  16822  xpsval  16826  ipoval  17747  frmdval  17999  symg2bas  18504  xpstopnlem2  22402  tusval  22858  tmsval  23074  tmsxpsval  23131  uniiccdif  24162  dchrval  25796  eengv  26751  wkslem1  27375  wkslem2  27376  iswlk  27378  wlkonl1iedg  27433  2wlklem  27435  redwlk  27440  wlkp1lem7  27447  wlkdlem2  27451  upgrwlkdvdelem  27503  usgr2pthlem  27530  usgr2pth  27531  crctcshwlkn0lem4  27577  crctcshwlkn0lem5  27578  crctcshwlkn0lem6  27579  iswwlks  27600  0enwwlksnge1  27628  wlkiswwlks2lem2  27634  wlkiswwlks2lem5  27637  wwlksm1edg  27645  wwlksnred  27656  wwlksnext  27657  wwlksnredwwlkn  27659  wwlksnextproplem2  27674  2wlkdlem10  27699  umgrwwlks2on  27721  rusgrnumwwlkl1  27732  isclwwlk  27747  clwwlkccatlem  27752  clwwlkccat  27753  clwlkclwwlklem2a1  27755  clwlkclwwlklem2fv1  27758  clwlkclwwlklem2a4  27760  clwlkclwwlklem2a  27761  clwlkclwwlklem2  27763  clwlkclwwlk  27765  clwwisshclwwslemlem  27776  clwwisshclwwslem  27777  clwwisshclwws  27778  clwwlkinwwlk  27803  clwwlkn2  27807  clwwlkel  27809  clwwlkf  27810  clwwlkwwlksb  27817  clwwlkext2edg  27819  wwlksext2clwwlk  27820  wwlksubclwwlk  27821  umgr2cwwk2dif  27827  s2elclwwlknon2  27867  clwwlknonex2lem2  27871  clwwlknonex2  27872  3wlkdlem10  27932  upgr3v3e3cycl  27943  upgr4cycl4dv4e  27948  eupthseg  27969  upgreupthseg  27972  eupth2lem3  27999  nfrgr2v  28035  frgr3vlem1  28036  frgr3vlem2  28037  4cycl2vnunb  28053  disjdifprg  30311  s2rn  30606  revwlk  32378  kur14lem1  32460  kur14  32470  bj-endval  34612  tgrpfset  37912  tgrpset  37913  hlhilset  39102  dfac21  39758  mendval  39875  mnurndlem1  40707  sge0sn  42751  isomuspgrlem2b  44079  isupwlk  44096  zlmodzxzsub  44493  prelrrx2b  44786  rrx2plordisom  44795  onsetreclem1  44892