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

Theorem prcom 4078
Description: Commutative law for unordered pairs. (Contributed by NM, 15-Jul-1993.)
Assertion
Ref Expression
prcom  |-  { A ,  B }  =  { B ,  A }

Proof of Theorem prcom
StepHypRef Expression
1 uncom 3610 . 2  |-  ( { A }  u.  { B } )  =  ( { B }  u.  { A } )
2 df-pr 4001 . 2  |-  { A ,  B }  =  ( { A }  u.  { B } )
3 df-pr 4001 . 2  |-  { B ,  A }  =  ( { B }  u.  { A } )
41, 2, 33eqtr4i 2461 1  |-  { A ,  B }  =  { B ,  A }
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437    u. cun 3434   {csn 3998   {cpr 4000
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-v 3082  df-un 3441  df-pr 4001
This theorem is referenced by:  preq2  4080  tpcoma  4096  tpidm23  4103  prid2g  4107  prid2  4109  prprc2  4111  difprsn2  4137  tpprceq3  4140  tppreqb  4141  preqr2  4175  preq12b  4176  prnebg  4182  fvpr2  6123  fvpr2g  6125  en2other2  8448  hashprb  12580  joincomALT  16274  meetcomALT  16276  symggen  17110  psgnran  17155  lspprid2  18220  lspexchn2  18353  lspindp2l  18356  lspindp2  18357  lsppratlem1  18369  psgnghm  19146  uvcvvcl  19343  mdetralt  19631  mdetunilem7  19641  usgraedgprv  25101  usgraedgrnv  25102  usgra2edg  25107  usgraedg4  25112  usgraidx2vlem1  25116  usgraidx2vlem2  25117  nbgraeledg  25156  nbgrassvwo2  25164  nbgrasym  25165  nbgracnvfv  25166  nbgraf1olem3  25169  nbgraf1olem5  25171  nb3graprlem1  25177  nb3graprlem2  25178  nb3grapr  25179  nb3grapr2  25180  nb3gra2nb  25181  cusgra2v  25188  cusgra3v  25190  uvtxnbgra  25219  uvtxnb  25223  2trllemH  25280  2trllemE  25281  wlkntrllem2  25288  usgrcyclnl2  25367  4cycl4dv  25393  cusconngra  25402  clwwlkn2  25501  vdgr1c  25631  vdegp1ci  25712  frgraunss  25721  frisusgranb  25723  frgra3v  25728  3vfriswmgra  25731  1to3vfriswmgra  25733  1to3vfriendship  25734  2pthfrgrarn  25735  2pthfrgra  25737  3cyclfrgrarn1  25738  4cycl2v2nb  25742  n4cyclfrgra  25744  frgranbnb  25746  frgrancvvdeqlem2  25757  frgrancvvdeqlem4  25759  frgrancvvdeqlem7  25762  frgrawopreglem4  25773  frgrawopreg  25775  frgrawopreg2  25777  frg2woteqm  25785  usg2spot2nb  25791  numclwwlkovf2ex  25812  pmtrprfv2  28619  indf  28845  indpreima  28854  measxun2  29040  measssd  29045  poimirlem9  31913  poimirlem15  31919  dihprrn  34963  dvh3dim  34983  dvh3dim3N  34986  lcfrlem21  35100  mapdindp4  35260  mapdh6eN  35277  mapdh7dN  35287  mapdh8ab  35314  mapdh8ad  35316  mapdh8b  35317  mapdh8e  35321  hdmap1l6e  35352  hdmap11lem2  35382  dfodd5  38659  ssprsseq  38868  usgr2edg  39074  usgredg4  39080  usgridx2vlem1  39085  usgridx2vlem2  39086  nbumgrel  39179  nbgr2vtx1edg  39182  nbuhgr2vtx1edgblem  39183  nbuhgr2vtx1edgb  39184  nbusgreledg  39185  nbgrssvwo2  39197  nbgrsym  39201  usgrnbcnvfv  39203  edgnbusgreu  39205  nbusgrf1o0  39207  nb3grprlem1  39213  nb3grprlem2  39214  nb3grpr  39215  nb3grpr2  39216  nb3gr2nb  39217  isuvtxa  39225  cusgredg  39248  usgredgsscusgredg  39276  usgra2pthlem1  39286  usgvincvad  39335  usgvincvadALT  39338  usgedgvadf1lem1  39344  usgedgvadf1lem2  39345  usgedgvadf1ALTlem1  39347  usgedgvadf1ALTlem2  39348
  Copyright terms: Public domain W3C validator