Theorem prcom 4700

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

Syntax hints:   = wceq 1567   ∪ cun 3911  {csn 4591  {cpr 4593

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-un 3918  df-pr 4594

This theorem is referenced by:  preq2  4702  tpcoma  4718  tpidm23  4725  prid2g  4729  prid2  4731  prprc2  4734  difprsn2  4770  tpprceq3  4773  tppreqb  4774  ssprsseq  4792  preq2b  4813  preqr2  4815  preq12b  4816  prnebg  4822  preq12nebg  4829  opthprneg  4831  elpreqpr  4833  elpr2elpr  4835  fvpr2g  7187  en2other2  9989  indf  12220  hashprb  14429  joincomALT  18451  meetcomALT  18453  symggen  19536  psgnran  19581  lspprid2  21093  lspexchn2  21229  lspindp2l  21232  lspindp2  21233  lsppratlem1  21245  psgnghm  21695  uvcvvcl  21902  mdetralt  22730  mdetunilem7  22740  uhgr2edg  29495  usgredg4  29504  usgredg2vlem1  29512  usgredg2vlem2  29513  nbupgrel  29632  nbgr2vtx1edg  29637  nbuhgr2vtx1edgblem  29638  nbuhgr2vtx1edgb  29639  nbusgreledg  29640  nbgrssvwo2  29649  nbgrsym  29650  usgrnbcnvfv  29652  edgnbusgreu  29654  nbusgrf1o0  29656  nb3grprlem1  29667  nb3grprlem2  29668  nb3grpr  29669  nb3grpr2  29670  nb3gr2nb  29671  isuvtx  29682  cusgredg  29711  usgredgsscusgredg  29746  1hegrvtxdg1r  29795  1egrvtxdg1r  29797  vdegp1ci  29825  usgr2wlkneq  30042  usgr2trlncl  30046  usgr2pthlem  30049  uspgrn2crct  30094  2wlkdlem6  30217  umgr2adedgspth  30234  wwlks2onsym  30246  clwwlkn2  30332  clwwlknonex2  30397  wlk2v2elem2  30444  uhgr3cyclexlem  30469  umgr3cyclex  30471  frcond1  30554  frcond3  30557  frgr3v  30563  3vfriswmgr  30566  1to3vfriswmgr  30568  1to3vfriendship  30569  2pthfrgrrn  30570  3cyclfrgrrn1  30573  4cycl2v2nb  30577  n4cyclfrgr  30579  frgrnbnb  30581  frgrncvvdeqlem3  30589  frgrncvvdeqlem6  30592  frgrwopregbsn  30605  frgrwopreglem5ALT  30610  fusgr2wsp2nb  30622  2clwwlk2clwwlklem  30634  indpreima  33122  indsupp  33124  pmtrprfv2  33345  cyc3genpmlem  33408  measxun2  34541  measssd  34546  revwlk  35512  cusgr3cyclex  35523  2cycl2d  35526  poimirlem9  38163  poimirlem15  38169  dihprrn  42085  dvh3dim  42105  dvh3dim3N  42108  lcfrlem21  42222  mapdindp4  42382  mapdh6eN  42399  mapdh7dN  42409  mapdh8ab  42436  mapdh8ad  42438  mapdh8b  42439  mapdh8e  42443  hdmap1l6e  42473  hdmap11lem2  42501  sprsymrelf  48126  paireqne  48142  reuopreuprim  48157  dfodd5  48307  clnbupgrel  48481  clnbgrsym  48485  grtriproplem  48586  grtrif1o  48589  grtriclwlk3  48592  cycl3grtrilem  48593  usgrgrtrirex  48597  isubgr3stgrlem6  48618  isubgr3stgrlem7  48619  grlimprclnbgr  48643  grlimprclnbgrvtx  48646  usgrexmpl2nb1  48679  usgrexmpl2nb2  48680  usgrexmpl2nb3  48681  usgrexmpl2nb4  48682  usgrexmpl2nb5  48683  gpgprismgriedgdmss  48699  gpgedgvtx0  48708  gpgedgvtx1  48709  gpgedg2ov  48713  gpgedg2iv  48714  gpg5nbgrvtx03starlem3  48717  gpg5nbgrvtx03star  48727  gpg5nbgr3star  48728  gpgprismgr4cycllem3  48744  gpgprismgr4cycllem8  48749  pgnbgreunbgrlem1  48760  pgnbgreunbgrlem2lem3  48763  pgnbgreunbgrlem2  48764  pgnbgreunbgrlem4  48766  pgnbgreunbgrlem5  48770  pgnbgreunbgr  48772  pgn4cyclex  48773  glbprlem  49621  toslat  49638