Theorem prcom 4628

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

Syntax hints:   = wceq 1538   ∪ cun 3879  {csn 4525  {cpr 4527

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-pr 4528

This theorem is referenced by:  preq2  4630  tpcoma  4646  tpidm23  4653  prid2g  4657  prid2  4659  prprc2  4662  difprsn2  4694  tpprceq3  4697  tppreqb  4698  ssprsseq  4718  preq2b  4738  preqr2  4740  preq12b  4741  prnebg  4746  preq12nebg  4753  opthprneg  4755  elpreqpr  4757  elpr2elpr  4759  fvpr2  6930  fvpr2g  6932  en2other2  9420  hashprb  13754  joincomALT  17631  meetcomALT  17633  symggen  18590  psgnran  18635  lspprid2  19763  lspexchn2  19896  lspindp2l  19899  lspindp2  19900  lsppratlem1  19912  psgnghm  20269  uvcvvcl  20476  mdetralt  21213  mdetunilem7  21223  uhgr2edg  26998  usgredg4  27007  usgredg2vlem1  27015  usgredg2vlem2  27016  nbupgrel  27135  nbgr2vtx1edg  27140  nbuhgr2vtx1edgblem  27141  nbuhgr2vtx1edgb  27142  nbusgreledg  27143  nbgrssvwo2  27152  nbgrsym  27153  usgrnbcnvfv  27155  edgnbusgreu  27157  nbusgrf1o0  27159  nb3grprlem1  27170  nb3grprlem2  27171  nb3grpr  27172  nb3grpr2  27173  nb3gr2nb  27174  isuvtx  27185  cusgredg  27214  usgredgsscusgredg  27249  1hegrvtxdg1r  27298  1egrvtxdg1r  27300  vdegp1ci  27328  usgr2wlkneq  27545  usgr2trlncl  27549  usgr2pthlem  27552  uspgrn2crct  27594  2wlkdlem6  27717  umgr2adedgspth  27734  wwlks2onsym  27744  clwwlkn2  27829  clwwlknonex2  27894  wlk2v2elem2  27941  uhgr3cyclexlem  27966  umgr3cyclex  27968  frcond1  28051  frcond3  28054  frgr3v  28060  3vfriswmgr  28063  1to3vfriswmgr  28065  1to3vfriendship  28066  2pthfrgrrn  28067  3cyclfrgrrn1  28070  4cycl2v2nb  28074  n4cyclfrgr  28076  frgrnbnb  28078  frgrncvvdeqlem3  28086  frgrncvvdeqlem6  28089  frgrwopregbsn  28102  frgrwopreglem5ALT  28107  fusgr2wsp2nb  28119  2clwwlk2clwwlklem  28131  pmtrprfv2  30782  cyc3genpmlem  30843  indf  31384  indpreima  31394  measxun2  31579  measssd  31584  revwlk  32484  cusgr3cyclex  32496  2cycl2d  32499  poimirlem9  35066  poimirlem15  35072  dihprrn  38722  dvh3dim  38742  dvh3dim3N  38745  lcfrlem21  38859  mapdindp4  39019  mapdh6eN  39036  mapdh7dN  39046  mapdh8ab  39073  mapdh8ad  39075  mapdh8b  39076  mapdh8e  39080  hdmap1l6e  39110  hdmap11lem2  39138  sprsymrelf  44012  paireqne  44028  reuopreuprim  44043  dfodd5  44178