Theorem preq12d 4722

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

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

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 2702

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 2709  df-cleq 2723  df-clel 2809  df-v 3461  df-un 3933  df-sn 4607  df-pr 4609

This theorem is referenced by:  opeq1  4850  csbopg  4868  opthhausdorff  5494  opthhausdorff0  5495  f1oprswap  6848  wunex2  10698  wuncval2  10707  s4prop  14826  wrdlen2  14860  wwlktovf  14872  wwlktovf1  14873  wwlktovfo  14874  wrd2f1tovbij  14876  prdsval  17366  xpsfval  17477  xpsval  17481  ipoval  18448  frmdval  18690  symg2bas  19203  xpstopnlem2  23214  tusval  23669  tmsval  23888  tmsxpsval  23946  uniiccdif  24994  dchrval  26634  eengv  28025  wkslem1  28652  wkslem2  28653  iswlk  28655  wlkonl1iedg  28710  2wlklem  28712  redwlk  28717  wlkp1lem7  28724  wlkdlem2  28728  upgrwlkdvdelem  28781  usgr2pthlem  28808  usgr2pth  28809  crctcshwlkn0lem4  28855  crctcshwlkn0lem5  28856  crctcshwlkn0lem6  28857  iswwlks  28878  0enwwlksnge1  28906  wlkiswwlks2lem2  28912  wlkiswwlks2lem5  28915  wwlksm1edg  28923  wwlksnred  28934  wwlksnext  28935  wwlksnredwwlkn  28937  wwlksnextproplem2  28952  2wlkdlem10  28977  umgrwwlks2on  28999  rusgrnumwwlkl1  29010  isclwwlk  29025  clwwlkccatlem  29030  clwwlkccat  29031  clwlkclwwlklem2a1  29033  clwlkclwwlklem2fv1  29036  clwlkclwwlklem2a4  29038  clwlkclwwlklem2a  29039  clwlkclwwlklem2  29041  clwlkclwwlk  29043  clwwisshclwwslemlem  29054  clwwisshclwwslem  29055  clwwisshclwws  29056  clwwlkinwwlk  29081  clwwlkn2  29085  clwwlkel  29087  clwwlkf  29088  clwwlkwwlksb  29095  clwwlkext2edg  29097  wwlksext2clwwlk  29098  wwlksubclwwlk  29099  umgr2cwwk2dif  29105  s2elclwwlknon2  29145  clwwlknonex2lem2  29149  clwwlknonex2  29150  3wlkdlem10  29210  upgr3v3e3cycl  29221  upgr4cycl4dv4e  29226  eupthseg  29247  upgreupthseg  29250  eupth2lem3  29277  nfrgr2v  29313  frgr3vlem1  29314  frgr3vlem2  29315  4cycl2vnunb  29331  disjdifprg  31594  s2rn  31904  idlsrgval  32355  revwlk  33839  kur14lem1  33921  kur14  33931  bj-endval  35893  tgrpfset  39313  tgrpset  39314  hlhilset  40503  dfac21  41484  mendval  41601  oaun2  41807  mnurndlem1  42716  sge0sn  44773  isomuspgrlem2b  46174  isupwlk  46191  zlmodzxzsub  46589  2arymaptf  46891  prelrrx2b  46953  rrx2plordisom  46962  onsetreclem1  47303