Theorem prcom 4731

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

Syntax hints:   = wceq 1539   ∪ cun 3948  {csn 4625  {cpr 4627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481  df-un 3955  df-pr 4628

This theorem is referenced by:  preq2  4733  tpcoma  4749  tpidm23  4756  prid2g  4760  prid2  4762  prprc2  4765  difprsn2  4800  tpprceq3  4803  tppreqb  4804  ssprsseq  4824  preq2b  4846  preqr2  4848  preq12b  4849  prnebg  4855  preq12nebg  4862  opthprneg  4864  elpreqpr  4866  elpr2elpr  4868  fvpr2g  7212  en2other2  10050  hashprb  14437  joincomALT  18447  meetcomALT  18449  symggen  19489  psgnran  19534  lspprid2  20997  lspexchn2  21134  lspindp2l  21137  lspindp2  21138  lsppratlem1  21150  psgnghm  21599  uvcvvcl  21808  mdetralt  22615  mdetunilem7  22625  uhgr2edg  29226  usgredg4  29235  usgredg2vlem1  29243  usgredg2vlem2  29244  nbupgrel  29363  nbgr2vtx1edg  29368  nbuhgr2vtx1edgblem  29369  nbuhgr2vtx1edgb  29370  nbusgreledg  29371  nbgrssvwo2  29380  nbgrsym  29381  usgrnbcnvfv  29383  edgnbusgreu  29385  nbusgrf1o0  29387  nb3grprlem1  29398  nb3grprlem2  29399  nb3grpr  29400  nb3grpr2  29401  nb3gr2nb  29402  isuvtx  29413  cusgredg  29442  usgredgsscusgredg  29478  1hegrvtxdg1r  29527  1egrvtxdg1r  29529  vdegp1ci  29557  usgr2wlkneq  29777  usgr2trlncl  29781  usgr2pthlem  29784  uspgrn2crct  29829  2wlkdlem6  29952  umgr2adedgspth  29969  wwlks2onsym  29979  clwwlkn2  30064  clwwlknonex2  30129  wlk2v2elem2  30176  uhgr3cyclexlem  30201  umgr3cyclex  30203  frcond1  30286  frcond3  30289  frgr3v  30295  3vfriswmgr  30298  1to3vfriswmgr  30300  1to3vfriendship  30301  2pthfrgrrn  30302  3cyclfrgrrn1  30305  4cycl2v2nb  30309  n4cyclfrgr  30311  frgrnbnb  30313  frgrncvvdeqlem3  30321  frgrncvvdeqlem6  30324  frgrwopregbsn  30337  frgrwopreglem5ALT  30342  fusgr2wsp2nb  30354  2clwwlk2clwwlklem  30366  indf  32841  indpreima  32851  indsupp  32853  pmtrprfv2  33109  cyc3genpmlem  33172  measxun2  34212  measssd  34217  revwlk  35131  cusgr3cyclex  35142  2cycl2d  35145  poimirlem9  37637  poimirlem15  37643  dihprrn  41429  dvh3dim  41449  dvh3dim3N  41452  lcfrlem21  41566  mapdindp4  41726  mapdh6eN  41743  mapdh7dN  41753  mapdh8ab  41780  mapdh8ad  41782  mapdh8b  41783  mapdh8e  41787  hdmap1l6e  41817  hdmap11lem2  41845  sprsymrelf  47487  paireqne  47503  reuopreuprim  47518  dfodd5  47652  clnbupgrel  47826  clnbgrsym  47829  grtriproplem  47911  grtrif1o  47914  grtriclwlk3  47917  cycl3grtrilem  47918  usgrgrtrirex  47922  isubgr3stgrlem6  47943  isubgr3stgrlem7  47944  usgrexmpl2nb1  47996  usgrexmpl2nb2  47997  usgrexmpl2nb3  47998  usgrexmpl2nb4  47999  usgrexmpl2nb5  48000  gpgedgvtx0  48024  gpgedgvtx1  48025  gpg5nbgrvtx03starlem3  48031  gpg5nbgrvtx03star  48041  gpg5nbgr3star  48042  glbprlem  48869  toslat  48886