Theorem prcom 4732

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

Syntax hints:   = wceq 1534   ∪ cun 3943  {csn 4624  {cpr 4626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3472  df-un 3950  df-pr 4627

This theorem is referenced by:  preq2  4734  tpcoma  4750  tpidm23  4757  prid2g  4761  prid2  4763  prprc2  4766  difprsn2  4800  tpprceq3  4803  tppreqb  4804  ssprsseq  4824  preq2b  4844  preqr2  4846  preq12b  4847  prnebg  4852  preq12nebg  4859  opthprneg  4861  elpreqpr  4863  elpr2elpr  4865  fvpr2g  7194  fvpr2gOLD  7195  fvpr2OLD  7199  en2other2  10026  hashprb  14382  joincomALT  18386  meetcomALT  18388  symggen  19418  psgnran  19463  lspprid2  20875  lspexchn2  21012  lspindp2l  21015  lspindp2  21016  lsppratlem1  21028  psgnghm  21505  uvcvvcl  21714  mdetralt  22503  mdetunilem7  22513  uhgr2edg  29014  usgredg4  29023  usgredg2vlem1  29031  usgredg2vlem2  29032  nbupgrel  29151  nbgr2vtx1edg  29156  nbuhgr2vtx1edgblem  29157  nbuhgr2vtx1edgb  29158  nbusgreledg  29159  nbgrssvwo2  29168  nbgrsym  29169  usgrnbcnvfv  29171  edgnbusgreu  29173  nbusgrf1o0  29175  nb3grprlem1  29186  nb3grprlem2  29187  nb3grpr  29188  nb3grpr2  29189  nb3gr2nb  29190  isuvtx  29201  cusgredg  29230  usgredgsscusgredg  29266  1hegrvtxdg1r  29315  1egrvtxdg1r  29317  vdegp1ci  29345  usgr2wlkneq  29563  usgr2trlncl  29567  usgr2pthlem  29570  uspgrn2crct  29612  2wlkdlem6  29735  umgr2adedgspth  29752  wwlks2onsym  29762  clwwlkn2  29847  clwwlknonex2  29912  wlk2v2elem2  29959  uhgr3cyclexlem  29984  umgr3cyclex  29986  frcond1  30069  frcond3  30072  frgr3v  30078  3vfriswmgr  30081  1to3vfriswmgr  30083  1to3vfriendship  30084  2pthfrgrrn  30085  3cyclfrgrrn1  30088  4cycl2v2nb  30092  n4cyclfrgr  30094  frgrnbnb  30096  frgrncvvdeqlem3  30104  frgrncvvdeqlem6  30107  frgrwopregbsn  30120  frgrwopreglem5ALT  30125  fusgr2wsp2nb  30137  2clwwlk2clwwlklem  30149  pmtrprfv2  32805  cyc3genpmlem  32866  indf  33628  indpreima  33638  measxun2  33823  measssd  33828  revwlk  34728  cusgr3cyclex  34740  2cycl2d  34743  poimirlem9  37096  poimirlem15  37102  dihprrn  40893  dvh3dim  40913  dvh3dim3N  40916  lcfrlem21  41030  mapdindp4  41190  mapdh6eN  41207  mapdh7dN  41217  mapdh8ab  41244  mapdh8ad  41246  mapdh8b  41247  mapdh8e  41251  hdmap1l6e  41281  hdmap11lem2  41309  sprsymrelf  46829  paireqne  46845  reuopreuprim  46860  dfodd5  46994  glbprlem  47978  toslat  47987

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »