Theorem prcom 4685

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

Syntax hints:   = wceq 1541   ∪ cun 3900  {csn 4576  {cpr 4578

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3907  df-pr 4579

This theorem is referenced by:  preq2  4687  tpcoma  4703  tpidm23  4710  prid2g  4714  prid2  4716  prprc2  4719  difprsn2  4753  tpprceq3  4756  tppreqb  4757  ssprsseq  4777  preq2b  4799  preqr2  4801  preq12b  4802  prnebg  4808  preq12nebg  4815  opthprneg  4817  elpreqpr  4819  elpr2elpr  4821  fvpr2g  7125  en2other2  9900  hashprb  14304  joincomALT  18305  meetcomALT  18307  symggen  19383  psgnran  19428  lspprid2  20932  lspexchn2  21069  lspindp2l  21072  lspindp2  21073  lsppratlem1  21085  psgnghm  21518  uvcvvcl  21725  mdetralt  22524  mdetunilem7  22534  uhgr2edg  29187  usgredg4  29196  usgredg2vlem1  29204  usgredg2vlem2  29205  nbupgrel  29324  nbgr2vtx1edg  29329  nbuhgr2vtx1edgblem  29330  nbuhgr2vtx1edgb  29331  nbusgreledg  29332  nbgrssvwo2  29341  nbgrsym  29342  usgrnbcnvfv  29344  edgnbusgreu  29346  nbusgrf1o0  29348  nb3grprlem1  29359  nb3grprlem2  29360  nb3grpr  29361  nb3grpr2  29362  nb3gr2nb  29363  isuvtx  29374  cusgredg  29403  usgredgsscusgredg  29439  1hegrvtxdg1r  29488  1egrvtxdg1r  29490  vdegp1ci  29518  usgr2wlkneq  29735  usgr2trlncl  29739  usgr2pthlem  29742  uspgrn2crct  29787  2wlkdlem6  29910  umgr2adedgspth  29927  wwlks2onsym  29937  clwwlkn2  30022  clwwlknonex2  30087  wlk2v2elem2  30134  uhgr3cyclexlem  30159  umgr3cyclex  30161  frcond1  30244  frcond3  30247  frgr3v  30253  3vfriswmgr  30256  1to3vfriswmgr  30258  1to3vfriendship  30259  2pthfrgrrn  30260  3cyclfrgrrn1  30263  4cycl2v2nb  30267  n4cyclfrgr  30269  frgrnbnb  30271  frgrncvvdeqlem3  30279  frgrncvvdeqlem6  30282  frgrwopregbsn  30295  frgrwopreglem5ALT  30300  fusgr2wsp2nb  30312  2clwwlk2clwwlklem  30324  indf  32834  indpreima  32844  indsupp  32846  pmtrprfv2  33055  cyc3genpmlem  33118  measxun2  34221  measssd  34226  revwlk  35167  cusgr3cyclex  35178  2cycl2d  35181  poimirlem9  37675  poimirlem15  37681  dihprrn  41471  dvh3dim  41491  dvh3dim3N  41494  lcfrlem21  41608  mapdindp4  41768  mapdh6eN  41785  mapdh7dN  41795  mapdh8ab  41822  mapdh8ad  41824  mapdh8b  41825  mapdh8e  41829  hdmap1l6e  41859  hdmap11lem2  41887  sprsymrelf  47532  paireqne  47548  reuopreuprim  47563  dfodd5  47697  clnbupgrel  47871  clnbgrsym  47875  grtriproplem  47976  grtrif1o  47979  grtriclwlk3  47982  cycl3grtrilem  47983  usgrgrtrirex  47987  isubgr3stgrlem6  48008  isubgr3stgrlem7  48009  grlimprclnbgr  48033  grlimprclnbgrvtx  48036  usgrexmpl2nb1  48069  usgrexmpl2nb2  48070  usgrexmpl2nb3  48071  usgrexmpl2nb4  48072  usgrexmpl2nb5  48073  gpgprismgriedgdmss  48089  gpgedgvtx0  48098  gpgedgvtx1  48099  gpgedg2ov  48103  gpgedg2iv  48104  gpg5nbgrvtx03starlem3  48107  gpg5nbgrvtx03star  48117  gpg5nbgr3star  48118  gpgprismgr4cycllem3  48134  gpgprismgr4cycllem8  48139  pgnbgreunbgrlem1  48150  pgnbgreunbgrlem2lem3  48153  pgnbgreunbgrlem2  48154  pgnbgreunbgrlem4  48156  pgnbgreunbgrlem5  48160  pgnbgreunbgr  48162  pgn4cyclex  48163  glbprlem  49002  toslat  49019