Theorem preq12d 4746

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

Syntax hints:   → wi 4   = wceq 1542  {cpr 4631

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3954  df-sn 4630  df-pr 4632

This theorem is referenced by:  opeq1  4874  csbopg  4892  opthhausdorff  5518  opthhausdorff0  5519  f1oprswap  6878  wunex2  10733  wuncval2  10742  s4prop  14861  wrdlen2  14895  wwlktovf  14907  wwlktovf1  14908  wwlktovfo  14909  wrd2f1tovbij  14911  prdsval  17401  xpsfval  17512  xpsval  17516  ipoval  18483  frmdval  18732  symg2bas  19260  xpstopnlem2  23315  tusval  23770  tmsval  23989  tmsxpsval  24047  uniiccdif  25095  dchrval  26737  eengv  28237  wkslem1  28864  wkslem2  28865  iswlk  28867  wlkonl1iedg  28922  2wlklem  28924  redwlk  28929  wlkp1lem7  28936  wlkdlem2  28940  upgrwlkdvdelem  28993  usgr2pthlem  29020  usgr2pth  29021  crctcshwlkn0lem4  29067  crctcshwlkn0lem5  29068  crctcshwlkn0lem6  29069  iswwlks  29090  0enwwlksnge1  29118  wlkiswwlks2lem2  29124  wlkiswwlks2lem5  29127  wwlksm1edg  29135  wwlksnred  29146  wwlksnext  29147  wwlksnredwwlkn  29149  wwlksnextproplem2  29164  2wlkdlem10  29189  umgrwwlks2on  29211  rusgrnumwwlkl1  29222  isclwwlk  29237  clwwlkccatlem  29242  clwwlkccat  29243  clwlkclwwlklem2a1  29245  clwlkclwwlklem2fv1  29248  clwlkclwwlklem2a4  29250  clwlkclwwlklem2a  29251  clwlkclwwlklem2  29253  clwlkclwwlk  29255  clwwisshclwwslemlem  29266  clwwisshclwwslem  29267  clwwisshclwws  29268  clwwlkinwwlk  29293  clwwlkn2  29297  clwwlkel  29299  clwwlkf  29300  clwwlkwwlksb  29307  clwwlkext2edg  29309  wwlksext2clwwlk  29310  wwlksubclwwlk  29311  umgr2cwwk2dif  29317  s2elclwwlknon2  29357  clwwlknonex2lem2  29361  clwwlknonex2  29362  3wlkdlem10  29422  upgr3v3e3cycl  29433  upgr4cycl4dv4e  29438  eupthseg  29459  upgreupthseg  29462  eupth2lem3  29489  nfrgr2v  29525  frgr3vlem1  29526  frgr3vlem2  29527  4cycl2vnunb  29543  disjdifprg  31806  s2rn  32110  idlsrgval  32617  revwlk  34115  kur14lem1  34197  kur14  34207  bj-endval  36196  tgrpfset  39615  tgrpset  39616  hlhilset  40805  dfac21  41808  mendval  41925  oaun2  42131  mnurndlem1  43040  sge0sn  45095  isomuspgrlem2b  46497  isupwlk  46514  zlmodzxzsub  47036  2arymaptf  47338  prelrrx2b  47400  rrx2plordisom  47409  onsetreclem1  47750