Theorem prcom 4691

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

Syntax hints:   = wceq 1542   ∪ cun 3901  {csn 4582  {cpr 4584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-pr 4585

This theorem is referenced by:  preq2  4693  tpcoma  4709  tpidm23  4716  prid2g  4720  prid2  4722  prprc2  4725  difprsn2  4759  tpprceq3  4762  tppreqb  4763  ssprsseq  4783  preq2b  4805  preqr2  4807  preq12b  4808  prnebg  4814  preq12nebg  4821  opthprneg  4823  elpreqpr  4825  elpr2elpr  4827  fvpr2g  7147  en2other2  9931  hashprb  14332  joincomALT  18334  meetcomALT  18336  symggen  19411  psgnran  19456  lspprid2  20961  lspexchn2  21098  lspindp2l  21101  lspindp2  21102  lsppratlem1  21114  psgnghm  21547  uvcvvcl  21754  mdetralt  22564  mdetunilem7  22574  uhgr2edg  29293  usgredg4  29302  usgredg2vlem1  29310  usgredg2vlem2  29311  nbupgrel  29430  nbgr2vtx1edg  29435  nbuhgr2vtx1edgblem  29436  nbuhgr2vtx1edgb  29437  nbusgreledg  29438  nbgrssvwo2  29447  nbgrsym  29448  usgrnbcnvfv  29450  edgnbusgreu  29452  nbusgrf1o0  29454  nb3grprlem1  29465  nb3grprlem2  29466  nb3grpr  29467  nb3grpr2  29468  nb3gr2nb  29469  isuvtx  29480  cusgredg  29509  usgredgsscusgredg  29545  1hegrvtxdg1r  29594  1egrvtxdg1r  29596  vdegp1ci  29624  usgr2wlkneq  29841  usgr2trlncl  29845  usgr2pthlem  29848  uspgrn2crct  29893  2wlkdlem6  30016  umgr2adedgspth  30033  wwlks2onsym  30045  clwwlkn2  30131  clwwlknonex2  30196  wlk2v2elem2  30243  uhgr3cyclexlem  30268  umgr3cyclex  30270  frcond1  30353  frcond3  30356  frgr3v  30362  3vfriswmgr  30365  1to3vfriswmgr  30367  1to3vfriendship  30368  2pthfrgrrn  30369  3cyclfrgrrn1  30372  4cycl2v2nb  30376  n4cyclfrgr  30378  frgrnbnb  30380  frgrncvvdeqlem3  30388  frgrncvvdeqlem6  30391  frgrwopregbsn  30404  frgrwopreglem5ALT  30409  fusgr2wsp2nb  30421  2clwwlk2clwwlklem  30433  indf  32944  indpreima  32957  indsupp  32959  pmtrprfv2  33181  cyc3genpmlem  33244  measxun2  34387  measssd  34392  revwlk  35338  cusgr3cyclex  35349  2cycl2d  35352  poimirlem9  37877  poimirlem15  37883  dihprrn  41799  dvh3dim  41819  dvh3dim3N  41822  lcfrlem21  41936  mapdindp4  42096  mapdh6eN  42113  mapdh7dN  42123  mapdh8ab  42150  mapdh8ad  42152  mapdh8b  42153  mapdh8e  42157  hdmap1l6e  42187  hdmap11lem2  42215  sprsymrelf  47852  paireqne  47868  reuopreuprim  47883  dfodd5  48017  clnbupgrel  48191  clnbgrsym  48195  grtriproplem  48296  grtrif1o  48299  grtriclwlk3  48302  cycl3grtrilem  48303  usgrgrtrirex  48307  isubgr3stgrlem6  48328  isubgr3stgrlem7  48329  grlimprclnbgr  48353  grlimprclnbgrvtx  48356  usgrexmpl2nb1  48389  usgrexmpl2nb2  48390  usgrexmpl2nb3  48391  usgrexmpl2nb4  48392  usgrexmpl2nb5  48393  gpgprismgriedgdmss  48409  gpgedgvtx0  48418  gpgedgvtx1  48419  gpgedg2ov  48423  gpgedg2iv  48424  gpg5nbgrvtx03starlem3  48427  gpg5nbgrvtx03star  48437  gpg5nbgr3star  48438  gpgprismgr4cycllem3  48454  gpgprismgr4cycllem8  48459  pgnbgreunbgrlem1  48470  pgnbgreunbgrlem2lem3  48473  pgnbgreunbgrlem2  48474  pgnbgreunbgrlem4  48476  pgnbgreunbgrlem5  48480  pgnbgreunbgr  48482  pgn4cyclex  48483  glbprlem  49321  toslat  49338