Theorem prcom 4693

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

This proof depends on syntax axioms:   = wceq 1570   ∪ cun 3897  {csn 4584  {cpr 4586

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3904  df-pr 4587

This theorem is used by:  preq2  4695  tpcoma  4711  tpidm23  4718  prid2g  4722  prid2  4724  prprc2  4727  difprsn2  4764  tpprceq3  4767  tppreqb  4768  ssprsseq  4786  preq2b  4807  preqr2  4809  preq12b  4810  prnebg  4816  preq12nebg  4823  opthprneg  4825  elpreqpr  4827  elpr2elpr  4829  fvpr2g  7189  en2other2  10012  indf  12248  hashprb  14461  joincomALT  18487  meetcomALT  18489  symggen  19597  psgnran  19642  lspprid2  21182  lspexchn2  21318  lspindp2l  21321  lspindp2  21322  lsppratlem1  21334  psgnghm  21793  uvcvvcl  22000  mdetralt  22830  mdetunilem7  22840  uhgr2edg  29668  usgredg4  29677  usgredg2vlem1  29685  usgredg2vlem2  29686  nbupgrel  29805  nbgr2vtx1edg  29810  nbuhgr2vtx1edgblem  29811  nbuhgr2vtx1edgb  29812  nbusgreledg  29813  nbgrssvwo2  29822  nbgrsym  29823  usgrnbcnvfv  29825  edgnbusgreu  29827  nbusgrf1o0  29829  nb3grprlem1  29840  nb3grprlem2  29841  nb3grpr  29842  nb3grpr2  29843  nb3gr2nb  29844  isuvtx  29855  cusgredg  29884  usgredgsscusgredg  29919  1hegrvtxdg1r  29968  1egrvtxdg1r  29970  vdegp1ci  29998  revwlk  30146  usgr2wlkneq  30221  usgr2trlncl  30225  usgr2pthlem  30228  uspgrn2crct  30276  2wlkdlem6  30399  umgr2adedgspth  30416  wwlks2onsym  30428  clwwlkn2  30514  clwwlknonex2  30579  umgr2cycllem  30625  wlk2v2elem2  30636  uhgr3cyclexlem  30661  umgr3cyclex  30663  frcond1  30746  frcond3  30749  frgr3v  30755  3vfriswmgr  30758  1to3vfriswmgr  30760  1to3vfriendship  30761  2pthfrgrrn  30762  3cyclfrgrrn1  30765  4cycl2v2nb  30769  n4cyclfrgr  30771  frgrnbnb  30773  frgrncvvdeqlem3  30781  frgrncvvdeqlem6  30784  frgrwopregbsn  30797  frgrwopreglem5ALT  30802  fusgr2wsp2nb  30814  2clwwlk2clwwlklem  30826  indpreima  33311  indsupp  33313  pmtrprfv2  33528  cyc3genpmlem  33591  measxun2  34721  measssd  34726  cusgr3cyclex  35725  2cycl2d  35726  poimirlem9  38378  poimirlem15  38384  dihprrn  42299  dvh3dim  42319  dvh3dim3N  42322  lcfrlem21  42436  mapdindp4  42596  mapdh6eN  42613  mapdh7dN  42623  mapdh8ab  42650  mapdh8ad  42652  mapdh8b  42653  mapdh8e  42657  hdmap1l6e  42687  hdmap11lem2  42715  sprsymrelf  48395  paireqne  48411  reuopreuprim  48426  dfodd5  48576  clnbupgrel  48750  clnbgrsym  48754  grtriproplem  48855  grtrif1o  48858  grtriclwlk3  48861  cycl3grtrilem  48862  usgrgrtrirex  48866  isubgr3stgrlem6  48887  isubgr3stgrlem7  48888  grlimprclnbgr  48912  grlimprclnbgrvtx  48915  usgrexmpl2nb1  48948  usgrexmpl2nb2  48949  usgrexmpl2nb3  48950  usgrexmpl2nb4  48951  usgrexmpl2nb5  48952  gpgprismgriedgdmss  48968  gpgedgvtx0  48977  gpgedgvtx1  48978  gpgedg2ov  48982  gpgedg2iv  48983  gpg5nbgrvtx03starlem3  48986  gpg5nbgrvtx03star  48996  gpg5nbgr3star  48997  gpgprismgr4cycllem3  49013  gpgprismgr4cycllem8  49018  pgnbgreunbgrlem1  49029  pgnbgreunbgrlem2lem3  49032  pgnbgreunbgrlem2  49033  pgnbgreunbgrlem4  49035  pgnbgreunbgrlem5  49039  pgnbgreunbgr  49041  pgn4cyclex  49042  glbprlem  49891  toslat  49908