MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  prcom Structured version   Visualization version   GIF version

Theorem prcom 4299
Description: Commutative law for unordered pairs. (Contributed by NM, 15-Jul-1993.)
Assertion
Ref Expression
prcom {𝐴, 𝐵} = {𝐵, 𝐴}

Proof of Theorem prcom
StepHypRef Expression
1 uncom 3790 . 2 ({𝐴} ∪ {𝐵}) = ({𝐵} ∪ {𝐴})
2 df-pr 4213 . 2 {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})
3 df-pr 4213 . 2 {𝐵, 𝐴} = ({𝐵} ∪ {𝐴})
41, 2, 33eqtr4i 2683 1 {𝐴, 𝐵} = {𝐵, 𝐴}
Colors of variables: wff setvar class
Syntax hints:   = wceq 1523  cun 3605  {csn 4210  {cpr 4212
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-un 3612  df-pr 4213
This theorem is referenced by:  preq2  4301  tpcoma  4317  tpidm23  4324  prid2g  4328  prid2  4330  prprc2  4333  difprsn2  4363  tpprceq3  4367  tppreqb  4368  ssprsseq  4389  preq2b  4410  preqr2  4412  preq12b  4413  prnebg  4420  elpreqpr  4427  elpr2elpr  4429  fvpr2  6498  fvpr2g  6500  en2other2  8870  hashprb  13223  joincomALT  17076  meetcomALT  17078  symggen  17936  psgnran  17981  lspprid2  19046  lspexchn2  19179  lspindp2l  19182  lspindp2  19183  lsppratlem1  19195  psgnghm  19974  uvcvvcl  20174  mdetralt  20462  mdetunilem7  20472  uhgr2edg  26145  usgredg4  26154  usgredg2vlem1  26162  usgredg2vlem2  26163  nbupgrel  26286  nbgr2vtx1edg  26291  nbuhgr2vtx1edgblem  26292  nbuhgr2vtx1edgb  26293  nbusgreledg  26294  nbgrssvwo2  26303  nbgrssvwo2OLD  26306  nbgrsym  26308  nbgrsymOLD  26309  usgrnbcnvfv  26311  edgnbusgreu  26313  nbusgrf1o0  26315  nb3grprlem1  26326  nb3grprlem2  26327  nb3grpr  26328  nb3grpr2  26329  nb3gr2nb  26330  isuvtx  26343  isuvtxaOLD  26344  cusgredg  26376  usgredgsscusgredg  26411  1hegrvtxdg1r  26460  1egrvtxdg1r  26462  vdegp1ci  26490  usgr2wlkneq  26708  usgr2trlncl  26712  usgr2pthlem  26715  uspgrn2crct  26756  2wlkdlem6  26896  umgr2adedgspth  26913  wwlks2onsym  26924  clwwlkn2  27007  clwwlknonex2  27084  wlk2v2elem2  27134  uhgr3cyclexlem  27159  umgr3cyclex  27161  frcond1  27246  frcond3  27249  frgr3v  27255  3vfriswmgr  27258  1to3vfriswmgr  27260  1to3vfriendship  27261  2pthfrgrrn  27262  3cyclfrgrrn1  27265  4cycl2v2nb  27269  n4cyclfrgr  27271  frgrnbnb  27273  frgrncvvdeqlem3  27281  frgrncvvdeqlem6  27284  frgrwopregbsn  27297  frgrwopreglem5ALT  27302  fusgr2wsp2nb  27314  extwwlkfablem1OLD  27323  2clwwlk2clwwlklem2lem2  27329  pmtrprfv2  29976  indf  30205  indpreima  30215  measxun2  30401  measssd  30406  poimirlem9  33548  poimirlem15  33554  dihprrn  37032  dvh3dim  37052  dvh3dim3N  37055  lcfrlem21  37169  mapdindp4  37329  mapdh6eN  37346  mapdh7dN  37356  mapdh8ab  37383  mapdh8ad  37385  mapdh8b  37386  mapdh8e  37390  hdmap1l6e  37421  hdmap11lem2  37451  dfodd5  41897  sprsymrelf  42070
  Copyright terms: Public domain W3C validator