Theorem prcom 4735

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

Syntax hints:   = wceq 1541   ∪ cun 3945  {csn 4627  {cpr 4629

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-un 3952  df-pr 4630

This theorem is referenced by:  preq2  4737  tpcoma  4753  tpidm23  4760  prid2g  4764  prid2  4766  prprc2  4769  difprsn2  4803  tpprceq3  4806  tppreqb  4807  ssprsseq  4827  preq2b  4847  preqr2  4849  preq12b  4850  prnebg  4855  preq12nebg  4862  opthprneg  4864  elpreqpr  4866  elpr2elpr  4868  fvpr2g  7185  fvpr2gOLD  7186  fvpr2OLD  7190  en2other2  10000  hashprb  14353  joincomALT  18350  meetcomALT  18352  symggen  19332  psgnran  19377  lspprid2  20601  lspexchn2  20736  lspindp2l  20739  lspindp2  20740  lsppratlem1  20752  psgnghm  21124  uvcvvcl  21333  mdetralt  22101  mdetunilem7  22111  uhgr2edg  28454  usgredg4  28463  usgredg2vlem1  28471  usgredg2vlem2  28472  nbupgrel  28591  nbgr2vtx1edg  28596  nbuhgr2vtx1edgblem  28597  nbuhgr2vtx1edgb  28598  nbusgreledg  28599  nbgrssvwo2  28608  nbgrsym  28609  usgrnbcnvfv  28611  edgnbusgreu  28613  nbusgrf1o0  28615  nb3grprlem1  28626  nb3grprlem2  28627  nb3grpr  28628  nb3grpr2  28629  nb3gr2nb  28630  isuvtx  28641  cusgredg  28670  usgredgsscusgredg  28705  1hegrvtxdg1r  28754  1egrvtxdg1r  28756  vdegp1ci  28784  usgr2wlkneq  29002  usgr2trlncl  29006  usgr2pthlem  29009  uspgrn2crct  29051  2wlkdlem6  29174  umgr2adedgspth  29191  wwlks2onsym  29201  clwwlkn2  29286  clwwlknonex2  29351  wlk2v2elem2  29398  uhgr3cyclexlem  29423  umgr3cyclex  29425  frcond1  29508  frcond3  29511  frgr3v  29517  3vfriswmgr  29520  1to3vfriswmgr  29522  1to3vfriendship  29523  2pthfrgrrn  29524  3cyclfrgrrn1  29527  4cycl2v2nb  29531  n4cyclfrgr  29533  frgrnbnb  29535  frgrncvvdeqlem3  29543  frgrncvvdeqlem6  29546  frgrwopregbsn  29559  frgrwopreglem5ALT  29564  fusgr2wsp2nb  29576  2clwwlk2clwwlklem  29588  pmtrprfv2  32236  cyc3genpmlem  32297  indf  33001  indpreima  33011  measxun2  33196  measssd  33201  revwlk  34103  cusgr3cyclex  34115  2cycl2d  34118  poimirlem9  36485  poimirlem15  36491  dihprrn  40285  dvh3dim  40305  dvh3dim3N  40308  lcfrlem21  40422  mapdindp4  40582  mapdh6eN  40599  mapdh7dN  40609  mapdh8ab  40636  mapdh8ad  40638  mapdh8b  40639  mapdh8e  40643  hdmap1l6e  40673  hdmap11lem2  40701  sprsymrelf  46149  paireqne  46165  reuopreuprim  46180  dfodd5  46314  glbprlem  47551  toslat  47560