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

Theorem prcom 3948
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 3495 . 2  |-  ( { A }  u.  { B } )  =  ( { B }  u.  { A } )
2 df-pr 3875 . 2  |-  { A ,  B }  =  ( { A }  u.  { B } )
3 df-pr 3875 . 2  |-  { B ,  A }  =  ( { B }  u.  { A } )
41, 2, 33eqtr4i 2468 1  |-  { A ,  B }  =  { B ,  A }
Colors of variables: wff setvar class
Syntax hints:    = wceq 1369    u. cun 3321   {csn 3872   {cpr 3874
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2969  df-un 3328  df-pr 3875
This theorem is referenced by:  preq2  3950  tpcoma  3966  tpidm23  3973  prid2g  3977  prid2  3979  prprc2  3981  difprsn2  4006  tpprceq3  4008  tppreqb  4009  preqr2  4042  preq12b  4043  prnebg  4049  fvpr2  5917  fvpr2g  5919  en2other2  8168  hashprb  12149  joincomALT  15191  meetcomALT  15193  symggen  15967  psgnran  16012  lspprid2  17056  lspexchn2  17189  lspindp2l  17192  lspindp2  17193  lsppratlem1  17205  psgnghm  17985  uvcvvcl  18187  mdetralt  18389  mdetunilem7  18399  usgraedgprv  23246  usgraedgrnv  23247  usgra2edg  23252  usgraedg4  23256  usgraidx2vlem1  23260  usgraidx2vlem2  23261  nbgraeledg  23292  nbgrasym  23299  nbgracnvfv  23300  nbgraf1olem3  23303  nbgraf1olem5  23305  nb3graprlem1  23310  nb3graprlem2  23311  nb3grapr  23312  nb3grapr2  23313  nb3gra2nb  23314  cusgra2v  23321  cusgra3v  23323  uvtxnbgra  23352  2trllemH  23402  2trllemE  23403  wlkntrllem2  23410  usgrcyclnl2  23478  4cycl4dv  23504  cusconngra  23513  vdgr1c  23526  vdegp1ci  23558  indf  26424  indpreima  26433  measxun2  26576  measssd  26581  nbgrassvwo2  30230  uvtxnb  30231  usgra2pthlem1  30253  clwwlkn2  30391  frgraunss  30540  frisusgranb  30542  frgra3v  30547  3vfriswmgra  30550  1to3vfriswmgra  30552  1to3vfriendship  30553  2pthfrgrarn  30554  2pthfrgra  30556  3cyclfrgrarn1  30557  4cycl2v2nb  30561  n4cyclfrgra  30563  frgranbnb  30565  frgrancvvdeqlem2  30577  frgrancvvdeqlem4  30579  frgrancvvdeqlem7  30582  frgrawopreglem4  30593  frgrawopreg  30595  frgrawopreg2  30597  frg2woteqm  30605  usg2spot2nb  30611  numclwwlkovf2ex  30632  dihprrn  34911  dvh3dim  34931  dvh3dim3N  34934  lcfrlem21  35048  mapdindp4  35208  mapdh6eN  35225  mapdh7dN  35235  mapdh8ab  35262  mapdh8ad  35264  mapdh8b  35265  mapdh8e  35269  hdmap1l6e  35300  hdmap11lem2  35330
  Copyright terms: Public domain W3C validator