Theorem preq12d 4745

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

Syntax hints:   → wi 4   = wceq 1541  {cpr 4630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-un 3953  df-sn 4629  df-pr 4631

This theorem is referenced by:  opeq1  4873  csbopg  4891  opthhausdorff  5517  opthhausdorff0  5518  f1oprswap  6877  wunex2  10735  wuncval2  10744  s4prop  14865  wrdlen2  14899  wwlktovf  14911  wwlktovf1  14912  wwlktovfo  14913  wrd2f1tovbij  14915  prdsval  17405  xpsfval  17516  xpsval  17520  ipoval  18487  frmdval  18768  symg2bas  19301  xpstopnlem2  23535  tusval  23990  tmsval  24209  tmsxpsval  24267  uniiccdif  25319  dchrval  26961  eengv  28492  wkslem1  29119  wkslem2  29120  iswlk  29122  wlkonl1iedg  29177  2wlklem  29179  redwlk  29184  wlkp1lem7  29191  wlkdlem2  29195  upgrwlkdvdelem  29248  usgr2pthlem  29275  usgr2pth  29276  crctcshwlkn0lem4  29322  crctcshwlkn0lem5  29323  crctcshwlkn0lem6  29324  iswwlks  29345  0enwwlksnge1  29373  wlkiswwlks2lem2  29379  wlkiswwlks2lem5  29382  wwlksm1edg  29390  wwlksnred  29401  wwlksnext  29402  wwlksnredwwlkn  29404  wwlksnextproplem2  29419  2wlkdlem10  29444  umgrwwlks2on  29466  rusgrnumwwlkl1  29477  isclwwlk  29492  clwwlkccatlem  29497  clwwlkccat  29498  clwlkclwwlklem2a1  29500  clwlkclwwlklem2fv1  29503  clwlkclwwlklem2a4  29505  clwlkclwwlklem2a  29506  clwlkclwwlklem2  29508  clwlkclwwlk  29510  clwwisshclwwslemlem  29521  clwwisshclwwslem  29522  clwwisshclwws  29523  clwwlkinwwlk  29548  clwwlkn2  29552  clwwlkel  29554  clwwlkf  29555  clwwlkwwlksb  29562  clwwlkext2edg  29564  wwlksext2clwwlk  29565  wwlksubclwwlk  29566  umgr2cwwk2dif  29572  s2elclwwlknon2  29612  clwwlknonex2lem2  29616  clwwlknonex2  29617  3wlkdlem10  29677  upgr3v3e3cycl  29688  upgr4cycl4dv4e  29693  eupthseg  29714  upgreupthseg  29717  eupth2lem3  29744  nfrgr2v  29780  frgr3vlem1  29781  frgr3vlem2  29782  4cycl2vnunb  29798  disjdifprg  32061  s2rn  32365  idlsrgval  32879  revwlk  34401  kur14lem1  34483  kur14  34493  bj-endval  36499  tgrpfset  39918  tgrpset  39919  hlhilset  41108  dfac21  42110  mendval  42227  oaun2  42433  mnurndlem1  43342  sge0sn  45394  isomuspgrlem2b  46796  isupwlk  46813  zlmodzxzsub  47125  2arymaptf  47426  prelrrx2b  47488  rrx2plordisom  47497  onsetreclem1  47838