Theorem preq12d 4695

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

Syntax hints:   → wi 4   = wceq 1540  {cpr 4581

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-un 3910  df-sn 4580  df-pr 4582

This theorem is referenced by:  opeq1  4827  csbopg  4845  opthhausdorff  5464  opthhausdorff0  5465  f1oprswap  6812  wunex2  10651  wuncval2  10660  s4prop  14835  wrdlen2  14869  wwlktovf  14881  wwlktovf1  14882  wwlktovfo  14883  wrd2f1tovbij  14885  prdsval  17377  xpsfval  17488  xpsval  17492  ipoval  18454  frmdval  18743  symg2bas  19290  xpstopnlem2  23714  tusval  24169  tmsval  24385  tmsxpsval  24442  uniiccdif  25495  dchrval  27161  eengv  28942  wkslem1  29571  wkslem2  29572  iswlk  29574  wlkonl1iedg  29627  2wlklem  29629  redwlk  29634  wlkp1lem7  29641  wlkdlem2  29645  upgrwlkdvdelem  29699  usgr2pthlem  29726  usgr2pth  29727  crctcshwlkn0lem4  29776  crctcshwlkn0lem5  29777  crctcshwlkn0lem6  29778  iswwlks  29799  0enwwlksnge1  29827  wlkiswwlks2lem2  29833  wlkiswwlks2lem5  29836  wwlksm1edg  29844  wwlksnred  29855  wwlksnext  29856  wwlksnredwwlkn  29858  wwlksnextproplem2  29873  2wlkdlem10  29898  umgrwwlks2on  29920  rusgrnumwwlkl1  29931  isclwwlk  29946  clwwlkccatlem  29951  clwwlkccat  29952  clwlkclwwlklem2a1  29954  clwlkclwwlklem2fv1  29957  clwlkclwwlklem2a4  29959  clwlkclwwlklem2a  29960  clwlkclwwlklem2  29962  clwlkclwwlk  29964  clwwisshclwwslemlem  29975  clwwisshclwwslem  29976  clwwisshclwws  29977  clwwlkinwwlk  30002  clwwlkn2  30006  clwwlkel  30008  clwwlkf  30009  clwwlkwwlksb  30016  clwwlkext2edg  30018  wwlksext2clwwlk  30019  wwlksubclwwlk  30020  umgr2cwwk2dif  30026  s2elclwwlknon2  30066  clwwlknonex2lem2  30070  clwwlknonex2  30071  3wlkdlem10  30131  upgr3v3e3cycl  30142  upgr4cycl4dv4e  30147  eupthseg  30168  upgreupthseg  30171  eupth2lem3  30198  nfrgr2v  30234  frgr3vlem1  30235  frgr3vlem2  30236  4cycl2vnunb  30252  disjdifprg  32537  s2rnOLD  32898  idlsrgval  33450  revwlk  35097  kur14lem1  35178  kur14  35188  bj-endval  37288  tgrpfset  40723  tgrpset  40724  hlhilset  41913  dfac21  43039  mendval  43152  oaun2  43354  mnurndlem1  44254  sge0sn  46361  isuspgrimlem  47880  upgrimwlklem5  47886  grtriproplem  47924  isgrtri  47928  grtriclwlk3  47930  cycl3grtrilem  47931  stgrfv  47938  gpgov  48027  gpgprismgriedgdmss  48037  gpgedgvtx0  48046  gpgedgvtx1  48047  gpgedgiov  48050  gpg3kgrtriexlem6  48073  gpg3kgrtriex  48074  gpgprismgr4cycllem3  48082  gpgprismgr4cycllem10  48089  pgnbgreunbgr  48110  gpg5edgnedg  48115  grlimedgnedg  48116  isupwlk  48121  zlmodzxzsub  48345  2arymaptf  48638  prelrrx2b  48700  rrx2plordisom  48709  onsetreclem1  49691