Theorem prcom 4648

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

Syntax hints:   = wceq 1543   ∪ cun 3864  {csn 4541  {cpr 4543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3410  df-un 3871  df-pr 4544

This theorem is referenced by:  preq2  4650  tpcoma  4666  tpidm23  4673  prid2g  4677  prid2  4679  prprc2  4682  difprsn2  4714  tpprceq3  4717  tppreqb  4718  ssprsseq  4738  preq2b  4758  preqr2  4760  preq12b  4761  prnebg  4766  preq12nebg  4773  opthprneg  4775  elpreqpr  4777  elpr2elpr  4779  fvpr2  7006  fvpr2g  7008  en2other2  9623  hashprb  13964  joincomALT  17907  meetcomALT  17909  symggen  18862  psgnran  18907  lspprid2  20035  lspexchn2  20168  lspindp2l  20171  lspindp2  20172  lsppratlem1  20184  psgnghm  20542  uvcvvcl  20749  mdetralt  21505  mdetunilem7  21515  uhgr2edg  27296  usgredg4  27305  usgredg2vlem1  27313  usgredg2vlem2  27314  nbupgrel  27433  nbgr2vtx1edg  27438  nbuhgr2vtx1edgblem  27439  nbuhgr2vtx1edgb  27440  nbusgreledg  27441  nbgrssvwo2  27450  nbgrsym  27451  usgrnbcnvfv  27453  edgnbusgreu  27455  nbusgrf1o0  27457  nb3grprlem1  27468  nb3grprlem2  27469  nb3grpr  27470  nb3grpr2  27471  nb3gr2nb  27472  isuvtx  27483  cusgredg  27512  usgredgsscusgredg  27547  1hegrvtxdg1r  27596  1egrvtxdg1r  27598  vdegp1ci  27626  usgr2wlkneq  27843  usgr2trlncl  27847  usgr2pthlem  27850  uspgrn2crct  27892  2wlkdlem6  28015  umgr2adedgspth  28032  wwlks2onsym  28042  clwwlkn2  28127  clwwlknonex2  28192  wlk2v2elem2  28239  uhgr3cyclexlem  28264  umgr3cyclex  28266  frcond1  28349  frcond3  28352  frgr3v  28358  3vfriswmgr  28361  1to3vfriswmgr  28363  1to3vfriendship  28364  2pthfrgrrn  28365  3cyclfrgrrn1  28368  4cycl2v2nb  28372  n4cyclfrgr  28374  frgrnbnb  28376  frgrncvvdeqlem3  28384  frgrncvvdeqlem6  28387  frgrwopregbsn  28400  frgrwopreglem5ALT  28405  fusgr2wsp2nb  28417  2clwwlk2clwwlklem  28429  pmtrprfv2  31076  cyc3genpmlem  31137  indf  31695  indpreima  31705  measxun2  31890  measssd  31895  revwlk  32799  cusgr3cyclex  32811  2cycl2d  32814  poimirlem9  35523  poimirlem15  35529  dihprrn  39177  dvh3dim  39197  dvh3dim3N  39200  lcfrlem21  39314  mapdindp4  39474  mapdh6eN  39491  mapdh7dN  39501  mapdh8ab  39528  mapdh8ad  39530  mapdh8b  39531  mapdh8e  39535  hdmap1l6e  39565  hdmap11lem2  39593  sprsymrelf  44620  paireqne  44636  reuopreuprim  44651  dfodd5  44785  glbprlem  45932  toslat  45941