Theorem prcom 4661

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

Syntax hints:   = wceq 1533   ∪ cun 3933  {csn 4560  {cpr 4562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-un 3940  df-pr 4563

This theorem is referenced by:  preq2  4663  tpcoma  4679  tpidm23  4686  prid2g  4690  prid2  4692  prprc2  4695  difprsn2  4727  tpprceq3  4730  tppreqb  4731  ssprsseq  4751  preq2b  4771  preqr2  4773  preq12b  4774  prnebg  4779  preq12nebg  4786  opthprneg  4788  elpreqpr  4790  elpr2elpr  4792  fvpr2  6947  fvpr2g  6949  en2other2  9429  hashprb  13752  joincomALT  17633  meetcomALT  17635  symggen  18592  psgnran  18637  lspprid2  19764  lspexchn2  19897  lspindp2l  19900  lspindp2  19901  lsppratlem1  19913  psgnghm  20718  uvcvvcl  20925  mdetralt  21211  mdetunilem7  21221  uhgr2edg  26984  usgredg4  26993  usgredg2vlem1  27001  usgredg2vlem2  27002  nbupgrel  27121  nbgr2vtx1edg  27126  nbuhgr2vtx1edgblem  27127  nbuhgr2vtx1edgb  27128  nbusgreledg  27129  nbgrssvwo2  27138  nbgrsym  27139  usgrnbcnvfv  27141  edgnbusgreu  27143  nbusgrf1o0  27145  nb3grprlem1  27156  nb3grprlem2  27157  nb3grpr  27158  nb3grpr2  27159  nb3gr2nb  27160  isuvtx  27171  cusgredg  27200  usgredgsscusgredg  27235  1hegrvtxdg1r  27284  1egrvtxdg1r  27286  vdegp1ci  27314  usgr2wlkneq  27531  usgr2trlncl  27535  usgr2pthlem  27538  uspgrn2crct  27580  2wlkdlem6  27704  umgr2adedgspth  27721  wwlks2onsym  27731  clwwlkn2  27816  clwwlknonex2  27882  wlk2v2elem2  27929  uhgr3cyclexlem  27954  umgr3cyclex  27956  frcond1  28039  frcond3  28042  frgr3v  28048  3vfriswmgr  28051  1to3vfriswmgr  28053  1to3vfriendship  28054  2pthfrgrrn  28055  3cyclfrgrrn1  28058  4cycl2v2nb  28062  n4cyclfrgr  28064  frgrnbnb  28066  frgrncvvdeqlem3  28074  frgrncvvdeqlem6  28077  frgrwopregbsn  28090  frgrwopreglem5ALT  28095  fusgr2wsp2nb  28107  2clwwlk2clwwlklem  28119  pmtrprfv2  30727  cyc3genpmlem  30788  indf  31269  indpreima  31279  measxun2  31464  measssd  31469  revwlk  32366  cusgr3cyclex  32378  2cycl2d  32381  poimirlem9  34895  poimirlem15  34901  dihprrn  38556  dvh3dim  38576  dvh3dim3N  38579  lcfrlem21  38693  mapdindp4  38853  mapdh6eN  38870  mapdh7dN  38880  mapdh8ab  38907  mapdh8ad  38909  mapdh8b  38910  mapdh8e  38914  hdmap1l6e  38944  hdmap11lem2  38972  sprsymrelf  43651  paireqne  43667  reuopreuprim  43682  dfodd5  43819