Theorem prcom 4757

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

Syntax hints:   = wceq 1537   ∪ cun 3974  {csn 4648  {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-pr 4651

This theorem is referenced by:  preq2  4759  tpcoma  4775  tpidm23  4782  prid2g  4786  prid2  4788  prprc2  4791  difprsn2  4826  tpprceq3  4829  tppreqb  4830  ssprsseq  4850  preq2b  4872  preqr2  4874  preq12b  4875  prnebg  4880  preq12nebg  4887  opthprneg  4889  elpreqpr  4891  elpr2elpr  4893  fvpr2g  7225  fvpr2gOLD  7226  fvpr2OLD  7230  en2other2  10078  hashprb  14446  joincomALT  18471  meetcomALT  18473  symggen  19512  psgnran  19557  lspprid2  21019  lspexchn2  21156  lspindp2l  21159  lspindp2  21160  lsppratlem1  21172  psgnghm  21621  uvcvvcl  21830  mdetralt  22635  mdetunilem7  22645  uhgr2edg  29243  usgredg4  29252  usgredg2vlem1  29260  usgredg2vlem2  29261  nbupgrel  29380  nbgr2vtx1edg  29385  nbuhgr2vtx1edgblem  29386  nbuhgr2vtx1edgb  29387  nbusgreledg  29388  nbgrssvwo2  29397  nbgrsym  29398  usgrnbcnvfv  29400  edgnbusgreu  29402  nbusgrf1o0  29404  nb3grprlem1  29415  nb3grprlem2  29416  nb3grpr  29417  nb3grpr2  29418  nb3gr2nb  29419  isuvtx  29430  cusgredg  29459  usgredgsscusgredg  29495  1hegrvtxdg1r  29544  1egrvtxdg1r  29546  vdegp1ci  29574  usgr2wlkneq  29792  usgr2trlncl  29796  usgr2pthlem  29799  uspgrn2crct  29841  2wlkdlem6  29964  umgr2adedgspth  29981  wwlks2onsym  29991  clwwlkn2  30076  clwwlknonex2  30141  wlk2v2elem2  30188  uhgr3cyclexlem  30213  umgr3cyclex  30215  frcond1  30298  frcond3  30301  frgr3v  30307  3vfriswmgr  30310  1to3vfriswmgr  30312  1to3vfriendship  30313  2pthfrgrrn  30314  3cyclfrgrrn1  30317  4cycl2v2nb  30321  n4cyclfrgr  30323  frgrnbnb  30325  frgrncvvdeqlem3  30333  frgrncvvdeqlem6  30336  frgrwopregbsn  30349  frgrwopreglem5ALT  30354  fusgr2wsp2nb  30366  2clwwlk2clwwlklem  30378  pmtrprfv2  33081  cyc3genpmlem  33144  indf  33979  indpreima  33989  measxun2  34174  measssd  34179  revwlk  35092  cusgr3cyclex  35104  2cycl2d  35107  poimirlem9  37589  poimirlem15  37595  dihprrn  41383  dvh3dim  41403  dvh3dim3N  41406  lcfrlem21  41520  mapdindp4  41680  mapdh6eN  41697  mapdh7dN  41707  mapdh8ab  41734  mapdh8ad  41736  mapdh8b  41737  mapdh8e  41741  hdmap1l6e  41771  hdmap11lem2  41799  sprsymrelf  47369  paireqne  47385  reuopreuprim  47400  dfodd5  47534  clnbupgrel  47707  clnbgrsym  47710  grtriproplem  47790  grtrif1o  47793  grtriclwlk3  47796  usgrgrtrirex  47799  usgrexmpl2nb1  47847  usgrexmpl2nb2  47848  usgrexmpl2nb3  47849  usgrexmpl2nb4  47850  usgrexmpl2nb5  47851  glbprlem  48645  toslat  48654