Theorem prcom 4665

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

Syntax hints:   = wceq 1539   ∪ cun 3881  {csn 4558  {cpr 4560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888  df-pr 4561

This theorem is referenced by:  preq2  4667  tpcoma  4683  tpidm23  4690  prid2g  4694  prid2  4696  prprc2  4699  difprsn2  4731  tpprceq3  4734  tppreqb  4735  ssprsseq  4755  preq2b  4775  preqr2  4777  preq12b  4778  prnebg  4783  preq12nebg  4790  opthprneg  4792  elpreqpr  4794  elpr2elpr  4796  fvpr2g  7045  fvpr2gOLD  7046  fvpr2OLD  7050  en2other2  9696  hashprb  14040  joincomALT  18034  meetcomALT  18036  symggen  18993  psgnran  19038  lspprid2  20175  lspexchn2  20308  lspindp2l  20311  lspindp2  20312  lsppratlem1  20324  psgnghm  20697  uvcvvcl  20904  mdetralt  21665  mdetunilem7  21675  uhgr2edg  27478  usgredg4  27487  usgredg2vlem1  27495  usgredg2vlem2  27496  nbupgrel  27615  nbgr2vtx1edg  27620  nbuhgr2vtx1edgblem  27621  nbuhgr2vtx1edgb  27622  nbusgreledg  27623  nbgrssvwo2  27632  nbgrsym  27633  usgrnbcnvfv  27635  edgnbusgreu  27637  nbusgrf1o0  27639  nb3grprlem1  27650  nb3grprlem2  27651  nb3grpr  27652  nb3grpr2  27653  nb3gr2nb  27654  isuvtx  27665  cusgredg  27694  usgredgsscusgredg  27729  1hegrvtxdg1r  27778  1egrvtxdg1r  27780  vdegp1ci  27808  usgr2wlkneq  28025  usgr2trlncl  28029  usgr2pthlem  28032  uspgrn2crct  28074  2wlkdlem6  28197  umgr2adedgspth  28214  wwlks2onsym  28224  clwwlkn2  28309  clwwlknonex2  28374  wlk2v2elem2  28421  uhgr3cyclexlem  28446  umgr3cyclex  28448  frcond1  28531  frcond3  28534  frgr3v  28540  3vfriswmgr  28543  1to3vfriswmgr  28545  1to3vfriendship  28546  2pthfrgrrn  28547  3cyclfrgrrn1  28550  4cycl2v2nb  28554  n4cyclfrgr  28556  frgrnbnb  28558  frgrncvvdeqlem3  28566  frgrncvvdeqlem6  28569  frgrwopregbsn  28582  frgrwopreglem5ALT  28587  fusgr2wsp2nb  28599  2clwwlk2clwwlklem  28611  pmtrprfv2  31259  cyc3genpmlem  31320  indf  31883  indpreima  31893  measxun2  32078  measssd  32083  revwlk  32986  cusgr3cyclex  32998  2cycl2d  33001  poimirlem9  35713  poimirlem15  35719  dihprrn  39367  dvh3dim  39387  dvh3dim3N  39390  lcfrlem21  39504  mapdindp4  39664  mapdh6eN  39681  mapdh7dN  39691  mapdh8ab  39718  mapdh8ad  39720  mapdh8b  39721  mapdh8e  39725  hdmap1l6e  39755  hdmap11lem2  39783  sprsymrelf  44835  paireqne  44851  reuopreuprim  44866  dfodd5  45000  glbprlem  46147  toslat  46156