Theorem prcom 4699

Description: Commutative law for unordered pairs. (Contributed by NM, 15-Jul-1993.)

Assertion

Ref	Expression
prcom	⊢ {𝐴, 𝐵} = {𝐵, 𝐴}

Proof of Theorem prcom

Step	Hyp	Ref	Expression
1		uncom 4113	. 2 ⊢ ({𝐴} ∪ {𝐵}) = ({𝐵} ∪ {𝐴})
2		df-pr 4593	. 2 ⊢ {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})
3		df-pr 4593	. 2 ⊢ {𝐵, 𝐴} = ({𝐵} ∪ {𝐴})
4	1, 2, 3	3eqtr4i 2796	1 ⊢ {𝐴, 𝐵} = {𝐵, 𝐴}

Syntax hints:   = wceq 1570   ∪ cun 3904  {csn 4590  {cpr 4592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3911  df-pr 4593

This theorem is referenced by:  preq2  4701  tpcoma  4717  tpidm23  4724  prid2g  4728  prid2  4730  prprc2  4733  difprsn2  4770  tpprceq3  4773  tppreqb  4774  ssprsseq  4792  preq2b  4813  preqr2  4815  preq12b  4816  prnebg  4822  preq12nebg  4829  opthprneg  4831  elpreqpr  4833  elpr2elpr  4835  fvpr2g  7191  en2other2  9994  indf  12225  hashprb  14435  joincomALT  18456  meetcomALT  18458  symggen  19541  psgnran  19586  lspprid2  21100  lspexchn2  21236  lspindp2l  21239  lspindp2  21240  lsppratlem1  21252  psgnghm  21711  uvcvvcl  21918  mdetralt  22746  mdetunilem7  22756  uhgr2edg  29539  usgredg4  29548  usgredg2vlem1  29556  usgredg2vlem2  29557  nbupgrel  29676  nbgr2vtx1edg  29681  nbuhgr2vtx1edgblem  29682  nbuhgr2vtx1edgb  29683  nbusgreledg  29684  nbgrssvwo2  29693  nbgrsym  29694  usgrnbcnvfv  29696  edgnbusgreu  29698  nbusgrf1o0  29700  nb3grprlem1  29711  nb3grprlem2  29712  nb3grpr  29713  nb3grpr2  29714  nb3gr2nb  29715  isuvtx  29726  cusgredg  29755  usgredgsscusgredg  29790  1hegrvtxdg1r  29839  1egrvtxdg1r  29841  vdegp1ci  29869  usgr2wlkneq  30086  usgr2trlncl  30090  usgr2pthlem  30093  uspgrn2crct  30138  2wlkdlem6  30261  umgr2adedgspth  30278  wwlks2onsym  30290  clwwlkn2  30376  clwwlknonex2  30441  wlk2v2elem2  30488  uhgr3cyclexlem  30513  umgr3cyclex  30515  frcond1  30598  frcond3  30601  frgr3v  30607  3vfriswmgr  30610  1to3vfriswmgr  30612  1to3vfriendship  30613  2pthfrgrrn  30614  3cyclfrgrrn1  30617  4cycl2v2nb  30621  n4cyclfrgr  30623  frgrnbnb  30625  frgrncvvdeqlem3  30633  frgrncvvdeqlem6  30636  frgrwopregbsn  30649  frgrwopreglem5ALT  30654  fusgr2wsp2nb  30666  2clwwlk2clwwlklem  30678  indpreima  33166  indsupp  33168  pmtrprfv2  33389  cyc3genpmlem  33452  measxun2  34581  measssd  34586  revwlk  35598  cusgr3cyclex  35609  2cycl2d  35612  poimirlem9  38261  poimirlem15  38267  dihprrn  42181  dvh3dim  42201  dvh3dim3N  42204  lcfrlem21  42318  mapdindp4  42478  mapdh6eN  42495  mapdh7dN  42505  mapdh8ab  42532  mapdh8ad  42534  mapdh8b  42535  mapdh8e  42539  hdmap1l6e  42569  hdmap11lem2  42597  sprsymrelf  48227  paireqne  48243  reuopreuprim  48258  dfodd5  48408  clnbupgrel  48582  clnbgrsym  48586  grtriproplem  48687  grtrif1o  48690  grtriclwlk3  48693  cycl3grtrilem  48694  usgrgrtrirex  48698  isubgr3stgrlem6  48719  isubgr3stgrlem7  48720  grlimprclnbgr  48744  grlimprclnbgrvtx  48747  usgrexmpl2nb1  48780  usgrexmpl2nb2  48781  usgrexmpl2nb3  48782  usgrexmpl2nb4  48783  usgrexmpl2nb5  48784  gpgprismgriedgdmss  48800  gpgedgvtx0  48809  gpgedgvtx1  48810  gpgedg2ov  48814  gpgedg2iv  48815  gpg5nbgrvtx03starlem3  48818  gpg5nbgrvtx03star  48828  gpg5nbgr3star  48829  gpgprismgr4cycllem3  48845  gpgprismgr4cycllem8  48850  pgnbgreunbgrlem1  48861  pgnbgreunbgrlem2lem3  48864  pgnbgreunbgrlem2  48865  pgnbgreunbgrlem4  48867  pgnbgreunbgrlem5  48871  pgnbgreunbgr  48873  pgn4cyclex  48874  glbprlem  49726  toslat  49743