Theorem prcom 4211

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

Syntax hints:   = wceq 1475   ∪ cun 3538  {csn 4125  {cpr 4127

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545  df-pr 4128

This theorem is referenced by:  preq2  4213  tpcoma  4229  tpidm23  4236  prid2g  4240  prid2  4242  prprc2  4244  difprsn2  4272  tpprceq3  4276  tppreqb  4277  ssprsseq  4297  preq2b  4318  preqr2  4321  preq12b  4322  prnebg  4329  elpreqpr  4334  elpr2elpr  4336  fvpr2  6362  fvpr2g  6364  en2other2  8715  hashprb  13046  joincomALT  16852  meetcomALT  16854  symggen  17713  psgnran  17758  lspprid2  18819  lspexchn2  18952  lspindp2l  18955  lspindp2  18956  lsppratlem1  18968  psgnghm  19745  uvcvvcl  19945  mdetralt  20233  mdetunilem7  20243  usgraedgprv  25905  usgraedgrnv  25906  usgra2edg  25911  usgraedg4  25916  usgraidx2vlem1  25920  usgraidx2vlem2  25921  nbgraeledg  25959  nbgrassvwo2  25967  nbgrasym  25968  nbgracnvfv  25969  nbgraf1olem3  25972  nbgraf1olem5  25974  nb3graprlem1  25980  nb3graprlem2  25981  nb3grapr  25982  nb3grapr2  25983  nb3gra2nb  25984  cusgra2v  25991  cusgra3v  25993  uvtxnbgra  26021  uvtxnb  26025  2trllemH  26082  2trllemE  26083  wlkntrllem2  26090  usgrcyclnl2  26169  4cycl4dv  26195  cusconngra  26204  clwwlkn2  26303  vdgr1c  26432  vdegp1ci  26513  frgraunss  26522  frisusgranb  26524  frgra3v  26529  3vfriswmgra  26532  1to3vfriswmgra  26534  1to3vfriendship  26535  2pthfrgrarn  26536  2pthfrgra  26538  3cyclfrgrarn1  26539  4cycl2v2nb  26543  n4cyclfrgra  26545  frgranbnb  26547  frgrancvvdeqlem2  26558  frgrancvvdeqlem4  26560  frgrancvvdeqlem7  26563  frgrawopreglem4  26574  frgrawopreg  26576  frgrawopreg2  26578  frg2woteqm  26586  usg2spot2nb  26592  numclwwlkovf2ex  26613  pmtrprfv2  29179  indf  29405  indpreima  29414  measxun2  29600  measssd  29605  poimirlem9  32588  poimirlem15  32594  dihprrn  35733  dvh3dim  35753  dvh3dim3N  35756  lcfrlem21  35870  mapdindp4  36030  mapdh6eN  36047  mapdh7dN  36057  mapdh8ab  36084  mapdh8ad  36086  mapdh8b  36087  mapdh8e  36091  hdmap1l6e  36122  hdmap11lem2  36152  dfodd5  40110  uhgr2edg  40435  usgredg4  40444  usgredg2vlem1  40452  usgredg2vlem2  40453  nbupgrel  40567  nbgr2vtx1edg  40572  nbuhgr2vtx1edgblem  40573  nbuhgr2vtx1edgb  40574  nbusgreledg  40575  nbgrssvwo2  40587  nbgrsym  40591  usgrnbcnvfv  40593  edgnbusgreu  40595  nbusgrf1o0  40597  nb3grprlem1  40608  nb3grprlem2  40609  nb3grpr  40610  nb3grpr2  40611  nb3gr2nb  40612  isuvtxa  40621  cusgredg  40646  usgredgsscusgredg  40675  1hegrvtxdg1r  40724  1egrvtxdg1r  40726  vdegp1ci-av  40754  usgr2wlkneq  40962  usgr2trlncl  40966  usgr2pthlem  40969  uspgrn2crct  41011  21wlkdlem6  41138  umgr2adedgspth  41155  clwwlksn2  41217  1wlk2v2elem2  41323  uhgr3cyclexlem  41348  umgr3cyclex  41350  frcond1  41438  frcond3  41440  frgr3v  41445  3vfriswmgr  41448  1to3vfriswmgr  41450  1to3vfriendship-av  41451  2pthfrgrrn  41452  3cyclfrgrrn1  41455  4cycl2v2nb-av  41459  n4cyclfrgr  41461  frgrnbnb  41463  frgrncvvdeqlem2  41470  frgrncvvdeqlem4  41472  frgrncvvdeqlem7  41475  frgrwopreglem4  41484  frgrwopreg  41486  frgrwopreg2  41488  frgr2wwlkeqm  41496  fusgr2wsp2nb  41498  av-extwwlkfablem1  41508  av-numclwwlkovf2ex  41517