Theorem prcom 4737

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

Syntax hints:   = wceq 1542   ∪ cun 3947  {csn 4629  {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-pr 4632

This theorem is referenced by:  preq2  4739  tpcoma  4755  tpidm23  4762  prid2g  4766  prid2  4768  prprc2  4771  difprsn2  4805  tpprceq3  4808  tppreqb  4809  ssprsseq  4829  preq2b  4849  preqr2  4851  preq12b  4852  prnebg  4857  preq12nebg  4864  opthprneg  4866  elpreqpr  4868  elpr2elpr  4870  fvpr2g  7189  fvpr2gOLD  7190  fvpr2OLD  7194  en2other2  10004  hashprb  14357  joincomALT  18354  meetcomALT  18356  symggen  19338  psgnran  19383  lspprid2  20609  lspexchn2  20744  lspindp2l  20747  lspindp2  20748  lsppratlem1  20760  psgnghm  21133  uvcvvcl  21342  mdetralt  22110  mdetunilem7  22120  uhgr2edg  28465  usgredg4  28474  usgredg2vlem1  28482  usgredg2vlem2  28483  nbupgrel  28602  nbgr2vtx1edg  28607  nbuhgr2vtx1edgblem  28608  nbuhgr2vtx1edgb  28609  nbusgreledg  28610  nbgrssvwo2  28619  nbgrsym  28620  usgrnbcnvfv  28622  edgnbusgreu  28624  nbusgrf1o0  28626  nb3grprlem1  28637  nb3grprlem2  28638  nb3grpr  28639  nb3grpr2  28640  nb3gr2nb  28641  isuvtx  28652  cusgredg  28681  usgredgsscusgredg  28716  1hegrvtxdg1r  28765  1egrvtxdg1r  28767  vdegp1ci  28795  usgr2wlkneq  29013  usgr2trlncl  29017  usgr2pthlem  29020  uspgrn2crct  29062  2wlkdlem6  29185  umgr2adedgspth  29202  wwlks2onsym  29212  clwwlkn2  29297  clwwlknonex2  29362  wlk2v2elem2  29409  uhgr3cyclexlem  29434  umgr3cyclex  29436  frcond1  29519  frcond3  29522  frgr3v  29528  3vfriswmgr  29531  1to3vfriswmgr  29533  1to3vfriendship  29534  2pthfrgrrn  29535  3cyclfrgrrn1  29538  4cycl2v2nb  29542  n4cyclfrgr  29544  frgrnbnb  29546  frgrncvvdeqlem3  29554  frgrncvvdeqlem6  29557  frgrwopregbsn  29570  frgrwopreglem5ALT  29575  fusgr2wsp2nb  29587  2clwwlk2clwwlklem  29599  pmtrprfv2  32249  cyc3genpmlem  32310  indf  33013  indpreima  33023  measxun2  33208  measssd  33213  revwlk  34115  cusgr3cyclex  34127  2cycl2d  34130  poimirlem9  36497  poimirlem15  36503  dihprrn  40297  dvh3dim  40317  dvh3dim3N  40320  lcfrlem21  40434  mapdindp4  40594  mapdh6eN  40611  mapdh7dN  40621  mapdh8ab  40648  mapdh8ad  40650  mapdh8b  40651  mapdh8e  40655  hdmap1l6e  40685  hdmap11lem2  40713  sprsymrelf  46163  paireqne  46179  reuopreuprim  46194  dfodd5  46328  glbprlem  47598  toslat  47607