Theorem prcom 4676

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 4098	. 2 ⊢ ({𝐴} ∪ {𝐵}) = ({𝐵} ∪ {𝐴})
2		df-pr 4570	. 2 ⊢ {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})
3		df-pr 4570	. 2 ⊢ {𝐵, 𝐴} = ({𝐵} ∪ {𝐴})
4	1, 2, 3	3eqtr4i 2769	1 ⊢ {𝐴, 𝐵} = {𝐵, 𝐴}

Syntax hints:   = wceq 1542   ∪ cun 3887  {csn 4567  {cpr 4569

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-pr 4570

This theorem is referenced by:  preq2  4678  tpcoma  4694  tpidm23  4701  prid2g  4705  prid2  4707  prprc2  4710  difprsn2  4746  tpprceq3  4749  tppreqb  4750  ssprsseq  4768  preq2b  4790  preqr2  4792  preq12b  4793  prnebg  4799  preq12nebg  4806  opthprneg  4808  elpreqpr  4810  elpr2elpr  4812  fvpr2g  7146  en2other2  9931  indf  12165  hashprb  14359  joincomALT  18365  meetcomALT  18367  symggen  19445  psgnran  19490  lspprid2  20993  lspexchn2  21129  lspindp2l  21132  lspindp2  21133  lsppratlem1  21145  psgnghm  21560  uvcvvcl  21767  mdetralt  22573  mdetunilem7  22583  uhgr2edg  29277  usgredg4  29286  usgredg2vlem1  29294  usgredg2vlem2  29295  nbupgrel  29414  nbgr2vtx1edg  29419  nbuhgr2vtx1edgblem  29420  nbuhgr2vtx1edgb  29421  nbusgreledg  29422  nbgrssvwo2  29431  nbgrsym  29432  usgrnbcnvfv  29434  edgnbusgreu  29436  nbusgrf1o0  29438  nb3grprlem1  29449  nb3grprlem2  29450  nb3grpr  29451  nb3grpr2  29452  nb3gr2nb  29453  isuvtx  29464  cusgredg  29493  usgredgsscusgredg  29528  1hegrvtxdg1r  29577  1egrvtxdg1r  29579  vdegp1ci  29607  usgr2wlkneq  29824  usgr2trlncl  29828  usgr2pthlem  29831  uspgrn2crct  29876  2wlkdlem6  29999  umgr2adedgspth  30016  wwlks2onsym  30028  clwwlkn2  30114  clwwlknonex2  30179  wlk2v2elem2  30226  uhgr3cyclexlem  30251  umgr3cyclex  30253  frcond1  30336  frcond3  30339  frgr3v  30345  3vfriswmgr  30348  1to3vfriswmgr  30350  1to3vfriendship  30351  2pthfrgrrn  30352  3cyclfrgrrn1  30355  4cycl2v2nb  30359  n4cyclfrgr  30361  frgrnbnb  30363  frgrncvvdeqlem3  30371  frgrncvvdeqlem6  30374  frgrwopregbsn  30387  frgrwopreglem5ALT  30392  fusgr2wsp2nb  30404  2clwwlk2clwwlklem  30416  indpreima  32925  indsupp  32927  pmtrprfv2  33149  cyc3genpmlem  33212  measxun2  34354  measssd  34359  revwlk  35307  cusgr3cyclex  35318  2cycl2d  35321  poimirlem9  37950  poimirlem15  37956  dihprrn  41872  dvh3dim  41892  dvh3dim3N  41895  lcfrlem21  42009  mapdindp4  42169  mapdh6eN  42186  mapdh7dN  42196  mapdh8ab  42223  mapdh8ad  42225  mapdh8b  42226  mapdh8e  42230  hdmap1l6e  42260  hdmap11lem2  42288  sprsymrelf  47955  paireqne  47971  reuopreuprim  47986  dfodd5  48136  clnbupgrel  48310  clnbgrsym  48314  grtriproplem  48415  grtrif1o  48418  grtriclwlk3  48421  cycl3grtrilem  48422  usgrgrtrirex  48426  isubgr3stgrlem6  48447  isubgr3stgrlem7  48448  grlimprclnbgr  48472  grlimprclnbgrvtx  48475  usgrexmpl2nb1  48508  usgrexmpl2nb2  48509  usgrexmpl2nb3  48510  usgrexmpl2nb4  48511  usgrexmpl2nb5  48512  gpgprismgriedgdmss  48528  gpgedgvtx0  48537  gpgedgvtx1  48538  gpgedg2ov  48542  gpgedg2iv  48543  gpg5nbgrvtx03starlem3  48546  gpg5nbgrvtx03star  48556  gpg5nbgr3star  48557  gpgprismgr4cycllem3  48573  gpgprismgr4cycllem8  48578  pgnbgreunbgrlem1  48589  pgnbgreunbgrlem2lem3  48592  pgnbgreunbgrlem2  48593  pgnbgreunbgrlem4  48595  pgnbgreunbgrlem5  48599  pgnbgreunbgr  48601  pgn4cyclex  48602  glbprlem  49440  toslat  49457