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 2794	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 2733

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 2740  df-cleq 2753  df-clel 2836  df-v 3453  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  7194  en2other2  10081  indf  12319  hashprb  14534  joincomALT  18566  meetcomALT  18568  symggen  19677  psgnran  19722  lspprid2  21266  lspexchn2  21402  lspindp2l  21405  lspindp2  21406  lsppratlem1  21418  psgnghm  21879  uvcvvcl  22086  mdetralt  22916  mdetunilem7  22926  uhgr2edg  29782  usgredg4  29791  usgredg2vlem1  29799  usgredg2vlem2  29800  nbupgrel  29919  nbgr2vtx1edg  29924  nbuhgr2vtx1edgblem  29925  nbuhgr2vtx1edgb  29926  nbusgreledg  29927  nbgrssvwo2  29936  nbgrsym  29937  usgrnbcnvfv  29939  edgnbusgreu  29941  nbusgrf1o0  29943  nb3grprlem1  29954  nb3grprlem2  29955  nb3grpr  29956  nb3grpr2  29957  nb3gr2nb  29958  isuvtx  29969  cusgredg  29998  usgredgsscusgredg  30033  1hegrvtxdg1r  30082  1egrvtxdg1r  30084  vdegp1ci  30112  revwlk  30260  usgr2wlkneq  30335  usgr2trlncl  30339  usgr2pthlem  30342  uspgrn2crct  30390  2wlkdlem6  30513  umgr2adedgspth  30530  wwlks2onsym  30542  clwwlkn2  30628  clwwlknonex2  30693  umgr2cycllem  30739  wlk2v2elem2  30750  uhgr3cyclexlem  30775  umgr3cyclex  30777  frcond1  30860  frcond3  30863  frgr3v  30869  3vfriswmgr  30872  1to3vfriswmgr  30874  1to3vfriendship  30875  2pthfrgrrn  30876  3cyclfrgrrn1  30879  4cycl2v2nb  30883  n4cyclfrgr  30885  frgrnbnb  30887  frgrncvvdeqlem3  30895  frgrncvvdeqlem6  30898  frgrwopregbsn  30911  frgrwopreglem5ALT  30916  fusgr2wsp2nb  30928  2clwwlk2clwwlklem  30940  indpreima  33425  indsupp  33427  pmtrprfv2  33642  cyc3genpmlem  33705  measxun2  34836  measssd  34841  cusgr3cyclex  35890  2cycl2d  35891  poimirlem9  38527  poimirlem15  38533  dihprrn  42463  dvh3dim  42483  dvh3dim3N  42486  lcfrlem21  42600  mapdindp4  42760  mapdh6eN  42777  mapdh7dN  42787  mapdh8ab  42814  mapdh8ad  42816  mapdh8b  42817  mapdh8e  42821  hdmap1l6e  42851  hdmap11lem2  42879  sprsymrelf  48546  paireqne  48562  reuopreuprim  48577  dfodd5  48727  clnbupgrel  48901  clnbgrsym  48905  grtriproplem  49006  grtrif1o  49009  grtriclwlk3  49012  cycl3grtrilem  49013  usgrgrtrirex  49017  isubgr3stgrlem6  49038  isubgr3stgrlem7  49039  grlimprclnbgr  49063  grlimprclnbgrvtx  49066  usgrexmpl2nb1  49099  usgrexmpl2nb2  49100  usgrexmpl2nb3  49101  usgrexmpl2nb4  49102  usgrexmpl2nb5  49103  gpgprismgriedgdmss  49119  gpgedgvtx0  49128  gpgedgvtx1  49129  gpgedg2ov  49133  gpgedg2iv  49134  gpg5nbgrvtx03starlem3  49137  gpg5nbgrvtx03star  49147  gpg5nbgr3star  49148  gpgprismgr4cycllem3  49164  gpgprismgr4cycllem8  49169  pgnbgreunbgrlem1  49180  pgnbgreunbgrlem2lem3  49183  pgnbgreunbgrlem2  49184  pgnbgreunbgrlem4  49186  pgnbgreunbgrlem5  49190  pgnbgreunbgr  49192  pgn4cyclex  49193  glbprlem  50042  toslat  50059