Theorem prcom 4267

Description: Commutative law for unordered pairs. (Contributed by NM, 15-Jul-1993.)

Assertion

Ref	Expression
prcom	|- { A , B } = { B , A }

Proof of Theorem prcom

Step	Hyp	Ref	Expression
1		uncom 3757	. 2 |- ( { A } u. { B } ) = ( { B } u. { A } )
2		df-pr 4180	. 2 |- { A , B } = ( { A } u. { B } )
3		df-pr 4180	. 2 |- { B , A } = ( { B } u. { A } )
4	1, 2, 3	3eqtr4i 2654	1 |- { A , B } = { B , A }

Syntax hints:   = wceq 1483   u. cun 3572   {csn 4177   {cpr 4179

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579  df-pr 4180

This theorem is referenced by:  preq2  4269  tpcoma  4285  tpidm23  4292  prid2g  4296  prid2  4298  prprc2  4301  difprsn2  4331  tpprceq3  4335  tppreqb  4336  ssprsseq  4357  preq2b  4378  preqr2  4381  preq12b  4382  prnebg  4389  elpreqpr  4396  elpr2elpr  4398  fvpr2  6457  fvpr2g  6459  en2other2  8832  hashprb  13185  joincomALT  17029  meetcomALT  17031  symggen  17890  psgnran  17935  lspprid2  18998  lspexchn2  19131  lspindp2l  19134  lspindp2  19135  lsppratlem1  19147  psgnghm  19926  uvcvvcl  20126  mdetralt  20414  mdetunilem7  20424  uhgr2edg  26100  usgredg4  26109  usgredg2vlem1  26117  usgredg2vlem2  26118  nbupgrel  26241  nbgr2vtx1edg  26246  nbuhgr2vtx1edgblem  26247  nbuhgr2vtx1edgb  26248  nbusgreledg  26249  nbgrssvwo2  26261  nbgrsym  26265  usgrnbcnvfv  26267  edgnbusgreu  26269  nbusgrf1o0  26271  nb3grprlem1  26282  nb3grprlem2  26283  nb3grpr  26284  nb3grpr2  26285  nb3gr2nb  26286  isuvtxa  26295  cusgredg  26320  usgredgsscusgredg  26355  1hegrvtxdg1r  26404  1egrvtxdg1r  26406  vdegp1ci  26434  usgr2wlkneq  26652  usgr2trlncl  26656  usgr2pthlem  26659  uspgrn2crct  26700  2wlkdlem6  26827  umgr2adedgspth  26844  wwlks2onsym  26851  clwwlksn2  26910  wlk2v2elem2  27016  uhgr3cyclexlem  27041  umgr3cyclex  27043  frcond1  27130  frcond3  27133  frgr3v  27139  3vfriswmgr  27142  1to3vfriswmgr  27144  1to3vfriendship  27145  2pthfrgrrn  27146  3cyclfrgrrn1  27149  4cycl2v2nb  27153  n4cyclfrgr  27155  frgrnbnb  27157  frgrncvvdeqlem3  27165  frgrncvvdeqlem6  27168  frgrwopregbsn  27181  frgrwopreglem5ALT  27186  fusgr2wsp2nb  27198  extwwlkfablem1  27207  numclwwlkovf2exlem2  27212  pmtrprfv2  29848  indf  30077  indpreima  30087  measxun2  30273  measssd  30278  poimirlem9  33418  poimirlem15  33424  dihprrn  36715  dvh3dim  36735  dvh3dim3N  36738  lcfrlem21  36852  mapdindp4  37012  mapdh6eN  37029  mapdh7dN  37039  mapdh8ab  37066  mapdh8ad  37068  mapdh8b  37069  mapdh8e  37073  hdmap1l6e  37104  hdmap11lem2  37134  dfodd5  41572  sprsymrelf  41745