Theorem preq12d 4766

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-sn 4649  df-pr 4651

This theorem is referenced by:  opeq1  4897  csbopg  4915  opthhausdorff  5536  opthhausdorff0  5537  f1oprswap  6906  wunex2  10807  wuncval2  10816  s4prop  14959  wrdlen2  14993  wwlktovf  15005  wwlktovf1  15006  wwlktovfo  15007  wrd2f1tovbij  15009  prdsval  17515  xpsfval  17626  xpsval  17630  ipoval  18600  frmdval  18886  symg2bas  19434  xpstopnlem2  23840  tusval  24295  tmsval  24514  tmsxpsval  24572  uniiccdif  25632  dchrval  27296  eengv  29012  wkslem1  29643  wkslem2  29644  iswlk  29646  wlkonl1iedg  29701  2wlklem  29703  redwlk  29708  wlkp1lem7  29715  wlkdlem2  29719  upgrwlkdvdelem  29772  usgr2pthlem  29799  usgr2pth  29800  crctcshwlkn0lem4  29846  crctcshwlkn0lem5  29847  crctcshwlkn0lem6  29848  iswwlks  29869  0enwwlksnge1  29897  wlkiswwlks2lem2  29903  wlkiswwlks2lem5  29906  wwlksm1edg  29914  wwlksnred  29925  wwlksnext  29926  wwlksnredwwlkn  29928  wwlksnextproplem2  29943  2wlkdlem10  29968  umgrwwlks2on  29990  rusgrnumwwlkl1  30001  isclwwlk  30016  clwwlkccatlem  30021  clwwlkccat  30022  clwlkclwwlklem2a1  30024  clwlkclwwlklem2fv1  30027  clwlkclwwlklem2a4  30029  clwlkclwwlklem2a  30030  clwlkclwwlklem2  30032  clwlkclwwlk  30034  clwwisshclwwslemlem  30045  clwwisshclwwslem  30046  clwwisshclwws  30047  clwwlkinwwlk  30072  clwwlkn2  30076  clwwlkel  30078  clwwlkf  30079  clwwlkwwlksb  30086  clwwlkext2edg  30088  wwlksext2clwwlk  30089  wwlksubclwwlk  30090  umgr2cwwk2dif  30096  s2elclwwlknon2  30136  clwwlknonex2lem2  30140  clwwlknonex2  30141  3wlkdlem10  30201  upgr3v3e3cycl  30212  upgr4cycl4dv4e  30217  eupthseg  30238  upgreupthseg  30241  eupth2lem3  30268  nfrgr2v  30304  frgr3vlem1  30305  frgr3vlem2  30306  4cycl2vnunb  30322  disjdifprg  32597  s2rnOLD  32910  idlsrgval  33496  revwlk  35092  kur14lem1  35174  kur14  35184  bj-endval  37281  tgrpfset  40701  tgrpset  40702  hlhilset  41891  dfac21  43023  mendval  43140  oaun2  43343  mnurndlem1  44250  sge0sn  46300  isuspgrimlem  47758  grtriproplem  47790  isgrtri  47794  grtriclwlk3  47796  isupwlk  47859  zlmodzxzsub  48085  2arymaptf  48386  prelrrx2b  48448  rrx2plordisom  48457  onsetreclem1  48797