Theorem prcom 4689

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 4151  df-pr 4587

This theorem is used by:  preq2  4691  tpcoma  4707  tpidm23  4714  prid2g  4718  prid2  4720  prprc2  4723  difprsn2  4760  tpprceq3  4763  tppreqb  4764  ssprsseq  4780  preq2b  4801  preqr2  4803  preq12b  4804  prnebg  4810  preq12nebg  4817  opthprneg  4819  elpreqpr  4821  elpr2elpr  4823  fvpr2g  7197  en2other2  10092  indf  12330  hashprb  14545  joincomALT  18579  meetcomALT  18581  symggen  19690  psgnran  19735  lspprid2  21279  lspexchn2  21415  lspindp2l  21418  lspindp2  21419  lsppratlem1  21431  psgnghm  21892  uvcvvcl  22099  mdetralt  22929  mdetunilem7  22939  uhgr2edg  29795  usgredg4  29804  usgredg2vlem1  29812  usgredg2vlem2  29813  nbupgrel  29932  nbgr2vtx1edg  29937  nbuhgr2vtx1edgblem  29938  nbuhgr2vtx1edgb  29939  nbusgreledg  29940  nbgrssvwo2  29949  nbgrsym  29950  usgrnbcnvfv  29952  edgnbusgreu  29954  nbusgrf1o0  29956  nb3grprlem1  29967  nb3grprlem2  29968  nb3grpr  29969  nb3grpr2  29970  nb3gr2nb  29971  isuvtx  29982  cusgredg  30011  usgredgsscusgredg  30046  1hegrvtxdg1r  30095  1egrvtxdg1r  30097  vdegp1ci  30125  revwlk  30273  usgr2wlkneq  30348  usgr2trlncl  30352  usgr2pthlem  30355  uspgrn2crct  30403  2wlkdlem6  30526  umgr2adedgspth  30543  wwlks2onsym  30555  clwwlkn2  30641  clwwlknonex2  30706  umgr2cycllem  30752  wlk2v2elem2  30763  uhgr3cyclexlem  30788  umgr3cyclex  30790  frcond1  30873  frcond3  30876  frgr3v  30882  3vfriswmgr  30885  1to3vfriswmgr  30887  1to3vfriendship  30888  2pthfrgrrn  30889  3cyclfrgrrn1  30892  4cycl2v2nb  30896  n4cyclfrgr  30898  frgrnbnb  30900  frgrncvvdeqlem3  30908  frgrncvvdeqlem6  30911  frgrwopregbsn  30924  frgrwopreglem5ALT  30929  fusgr2wsp2nb  30941  2clwwlk2clwwlklem  30953  indpreima  33479  indsupp  33481  pmtrprfv2  33696  cyc3genpmlem  33759  measxun2  34890  measssd  34895  cusgr3cyclex  35988  2cycl2d  35989  poimirlem9  38641  poimirlem15  38647  dihprrn  42577  dvh3dim  42597  dvh3dim3N  42600  lcfrlem21  42714  mapdindp4  42874  mapdh6eN  42891  mapdh7dN  42901  mapdh8ab  42928  mapdh8ad  42930  mapdh8b  42931  mapdh8e  42935  hdmap1l6e  42965  hdmap11lem2  42993  sprsymrelf  48671  paireqne  48687  reuopreuprim  48702  dfodd5  48852  clnbupgrel  49026  clnbgrsym  49030  grtriproplem  49131  grtrif1o  49134  grtriclwlk3  49137  cycl3grtrilem  49138  usgrgrtrirex  49142  isubgr3stgrlem6  49163  isubgr3stgrlem7  49164  grlimprclnbgr  49188  grlimprclnbgrvtx  49191  usgrexmpl2nb1  49224  usgrexmpl2nb2  49225  usgrexmpl2nb3  49226  usgrexmpl2nb4  49227  usgrexmpl2nb5  49228  gpgprismgriedgdmss  49244  gpgedgvtx0  49253  gpgedgvtx1  49254  gpgedg2ov  49258  gpgedg2iv  49259  gpg5nbgrvtx03starlem3  49262  gpg5nbgrvtx03star  49272  gpg5nbgr3star  49273  gpgprismgr4cycllem3  49289  gpgprismgr4cycllem8  49294  pgnbgreunbgrlem1  49305  pgnbgreunbgrlem2lem3  49308  pgnbgreunbgrlem2  49309  pgnbgreunbgrlem4  49311  pgnbgreunbgrlem5  49315  pgnbgreunbgr  49317  pgn4cyclex  49318  glbprlem  50173  toslat  50190