Theorem prcom 4713

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

Syntax hints:   = wceq 1540   ∪ cun 3929  {csn 4606  {cpr 4608

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-un 3936  df-pr 4609

This theorem is referenced by:  preq2  4715  tpcoma  4731  tpidm23  4738  prid2g  4742  prid2  4744  prprc2  4747  difprsn2  4782  tpprceq3  4785  tppreqb  4786  ssprsseq  4806  preq2b  4828  preqr2  4830  preq12b  4831  prnebg  4837  preq12nebg  4844  opthprneg  4846  elpreqpr  4848  elpr2elpr  4850  fvpr2g  7188  en2other2  10028  hashprb  14420  joincomALT  18416  meetcomALT  18418  symggen  19456  psgnran  19501  lspprid2  20960  lspexchn2  21097  lspindp2l  21100  lspindp2  21101  lsppratlem1  21113  psgnghm  21545  uvcvvcl  21752  mdetralt  22551  mdetunilem7  22561  uhgr2edg  29192  usgredg4  29201  usgredg2vlem1  29209  usgredg2vlem2  29210  nbupgrel  29329  nbgr2vtx1edg  29334  nbuhgr2vtx1edgblem  29335  nbuhgr2vtx1edgb  29336  nbusgreledg  29337  nbgrssvwo2  29346  nbgrsym  29347  usgrnbcnvfv  29349  edgnbusgreu  29351  nbusgrf1o0  29353  nb3grprlem1  29364  nb3grprlem2  29365  nb3grpr  29366  nb3grpr2  29367  nb3gr2nb  29368  isuvtx  29379  cusgredg  29408  usgredgsscusgredg  29444  1hegrvtxdg1r  29493  1egrvtxdg1r  29495  vdegp1ci  29523  usgr2wlkneq  29743  usgr2trlncl  29747  usgr2pthlem  29750  uspgrn2crct  29795  2wlkdlem6  29918  umgr2adedgspth  29935  wwlks2onsym  29945  clwwlkn2  30030  clwwlknonex2  30095  wlk2v2elem2  30142  uhgr3cyclexlem  30167  umgr3cyclex  30169  frcond1  30252  frcond3  30255  frgr3v  30261  3vfriswmgr  30264  1to3vfriswmgr  30266  1to3vfriendship  30267  2pthfrgrrn  30268  3cyclfrgrrn1  30271  4cycl2v2nb  30275  n4cyclfrgr  30277  frgrnbnb  30279  frgrncvvdeqlem3  30287  frgrncvvdeqlem6  30290  frgrwopregbsn  30303  frgrwopreglem5ALT  30308  fusgr2wsp2nb  30320  2clwwlk2clwwlklem  30332  indf  32837  indpreima  32847  indsupp  32849  pmtrprfv2  33104  cyc3genpmlem  33167  measxun2  34246  measssd  34251  revwlk  35152  cusgr3cyclex  35163  2cycl2d  35166  poimirlem9  37658  poimirlem15  37664  dihprrn  41450  dvh3dim  41470  dvh3dim3N  41473  lcfrlem21  41587  mapdindp4  41747  mapdh6eN  41764  mapdh7dN  41774  mapdh8ab  41801  mapdh8ad  41803  mapdh8b  41804  mapdh8e  41808  hdmap1l6e  41838  hdmap11lem2  41866  sprsymrelf  47476  paireqne  47492  reuopreuprim  47507  dfodd5  47641  clnbupgrel  47815  clnbgrsym  47818  grtriproplem  47918  grtrif1o  47921  grtriclwlk3  47924  cycl3grtrilem  47925  usgrgrtrirex  47929  isubgr3stgrlem6  47950  isubgr3stgrlem7  47951  usgrexmpl2nb1  48003  usgrexmpl2nb2  48004  usgrexmpl2nb3  48005  usgrexmpl2nb4  48006  usgrexmpl2nb5  48007  gpgprismgriedgdmss  48023  gpgedgvtx0  48032  gpgedgvtx1  48033  gpg5nbgrvtx03starlem3  48039  gpg5nbgrvtx03star  48049  gpg5nbgr3star  48050  gpgprismgr4cycllem3  48063  gpgprismgr4cycllem8  48068  glbprlem  48906  toslat  48923