Theorem prcom 4668

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

Syntax hints:   = wceq 1539   ∪ cun 3885  {csn 4561  {cpr 4563

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-un 3892  df-pr 4564

This theorem is referenced by:  preq2  4670  tpcoma  4686  tpidm23  4693  prid2g  4697  prid2  4699  prprc2  4702  difprsn2  4734  tpprceq3  4737  tppreqb  4738  ssprsseq  4758  preq2b  4778  preqr2  4780  preq12b  4781  prnebg  4786  preq12nebg  4793  opthprneg  4795  elpreqpr  4797  elpr2elpr  4799  fvpr2g  7063  fvpr2gOLD  7064  fvpr2OLD  7068  en2other2  9765  hashprb  14112  joincomALT  18119  meetcomALT  18121  symggen  19078  psgnran  19123  lspprid2  20260  lspexchn2  20393  lspindp2l  20396  lspindp2  20397  lsppratlem1  20409  psgnghm  20785  uvcvvcl  20994  mdetralt  21757  mdetunilem7  21767  uhgr2edg  27575  usgredg4  27584  usgredg2vlem1  27592  usgredg2vlem2  27593  nbupgrel  27712  nbgr2vtx1edg  27717  nbuhgr2vtx1edgblem  27718  nbuhgr2vtx1edgb  27719  nbusgreledg  27720  nbgrssvwo2  27729  nbgrsym  27730  usgrnbcnvfv  27732  edgnbusgreu  27734  nbusgrf1o0  27736  nb3grprlem1  27747  nb3grprlem2  27748  nb3grpr  27749  nb3grpr2  27750  nb3gr2nb  27751  isuvtx  27762  cusgredg  27791  usgredgsscusgredg  27826  1hegrvtxdg1r  27875  1egrvtxdg1r  27877  vdegp1ci  27905  usgr2wlkneq  28124  usgr2trlncl  28128  usgr2pthlem  28131  uspgrn2crct  28173  2wlkdlem6  28296  umgr2adedgspth  28313  wwlks2onsym  28323  clwwlkn2  28408  clwwlknonex2  28473  wlk2v2elem2  28520  uhgr3cyclexlem  28545  umgr3cyclex  28547  frcond1  28630  frcond3  28633  frgr3v  28639  3vfriswmgr  28642  1to3vfriswmgr  28644  1to3vfriendship  28645  2pthfrgrrn  28646  3cyclfrgrrn1  28649  4cycl2v2nb  28653  n4cyclfrgr  28655  frgrnbnb  28657  frgrncvvdeqlem3  28665  frgrncvvdeqlem6  28668  frgrwopregbsn  28681  frgrwopreglem5ALT  28686  fusgr2wsp2nb  28698  2clwwlk2clwwlklem  28710  pmtrprfv2  31357  cyc3genpmlem  31418  indf  31983  indpreima  31993  measxun2  32178  measssd  32183  revwlk  33086  cusgr3cyclex  33098  2cycl2d  33101  poimirlem9  35786  poimirlem15  35792  dihprrn  39440  dvh3dim  39460  dvh3dim3N  39463  lcfrlem21  39577  mapdindp4  39737  mapdh6eN  39754  mapdh7dN  39764  mapdh8ab  39791  mapdh8ad  39793  mapdh8b  39794  mapdh8e  39798  hdmap1l6e  39828  hdmap11lem2  39856  sprsymrelf  44947  paireqne  44963  reuopreuprim  44978  dfodd5  45112  glbprlem  46259  toslat  46268