Theorem prcom 4696

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

Syntax hints:   = wceq 1540   ∪ cun 3912  {csn 4589  {cpr 4591

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919  df-pr 4592

This theorem is referenced by:  preq2  4698  tpcoma  4714  tpidm23  4721  prid2g  4725  prid2  4727  prprc2  4730  difprsn2  4765  tpprceq3  4768  tppreqb  4769  ssprsseq  4789  preq2b  4811  preqr2  4813  preq12b  4814  prnebg  4820  preq12nebg  4827  opthprneg  4829  elpreqpr  4831  elpr2elpr  4833  fvpr2g  7165  en2other2  9962  hashprb  14362  joincomALT  18360  meetcomALT  18362  symggen  19400  psgnran  19445  lspprid2  20904  lspexchn2  21041  lspindp2l  21044  lspindp2  21045  lsppratlem1  21057  psgnghm  21489  uvcvvcl  21696  mdetralt  22495  mdetunilem7  22505  uhgr2edg  29135  usgredg4  29144  usgredg2vlem1  29152  usgredg2vlem2  29153  nbupgrel  29272  nbgr2vtx1edg  29277  nbuhgr2vtx1edgblem  29278  nbuhgr2vtx1edgb  29279  nbusgreledg  29280  nbgrssvwo2  29289  nbgrsym  29290  usgrnbcnvfv  29292  edgnbusgreu  29294  nbusgrf1o0  29296  nb3grprlem1  29307  nb3grprlem2  29308  nb3grpr  29309  nb3grpr2  29310  nb3gr2nb  29311  isuvtx  29322  cusgredg  29351  usgredgsscusgredg  29387  1hegrvtxdg1r  29436  1egrvtxdg1r  29438  vdegp1ci  29466  usgr2wlkneq  29686  usgr2trlncl  29690  usgr2pthlem  29693  uspgrn2crct  29738  2wlkdlem6  29861  umgr2adedgspth  29878  wwlks2onsym  29888  clwwlkn2  29973  clwwlknonex2  30038  wlk2v2elem2  30085  uhgr3cyclexlem  30110  umgr3cyclex  30112  frcond1  30195  frcond3  30198  frgr3v  30204  3vfriswmgr  30207  1to3vfriswmgr  30209  1to3vfriendship  30210  2pthfrgrrn  30211  3cyclfrgrrn1  30214  4cycl2v2nb  30218  n4cyclfrgr  30220  frgrnbnb  30222  frgrncvvdeqlem3  30230  frgrncvvdeqlem6  30233  frgrwopregbsn  30246  frgrwopreglem5ALT  30251  fusgr2wsp2nb  30263  2clwwlk2clwwlklem  30275  indf  32778  indpreima  32788  indsupp  32790  pmtrprfv2  33045  cyc3genpmlem  33108  measxun2  34200  measssd  34205  revwlk  35112  cusgr3cyclex  35123  2cycl2d  35126  poimirlem9  37623  poimirlem15  37629  dihprrn  41420  dvh3dim  41440  dvh3dim3N  41443  lcfrlem21  41557  mapdindp4  41717  mapdh6eN  41734  mapdh7dN  41744  mapdh8ab  41771  mapdh8ad  41773  mapdh8b  41774  mapdh8e  41778  hdmap1l6e  41808  hdmap11lem2  41836  sprsymrelf  47493  paireqne  47509  reuopreuprim  47524  dfodd5  47658  clnbupgrel  47832  clnbgrsym  47835  grtriproplem  47935  grtrif1o  47938  grtriclwlk3  47941  cycl3grtrilem  47942  usgrgrtrirex  47946  isubgr3stgrlem6  47967  isubgr3stgrlem7  47968  usgrexmpl2nb1  48020  usgrexmpl2nb2  48021  usgrexmpl2nb3  48022  usgrexmpl2nb4  48023  usgrexmpl2nb5  48024  gpgprismgriedgdmss  48040  gpgedgvtx0  48049  gpgedgvtx1  48050  gpgedg2ov  48054  gpgedg2iv  48055  gpg5nbgrvtx03starlem3  48058  gpg5nbgrvtx03star  48068  gpg5nbgr3star  48069  gpgprismgr4cycllem3  48084  gpgprismgr4cycllem8  48089  pgnbgreunbgrlem1  48100  pgnbgreunbgrlem2lem3  48103  pgnbgreunbgrlem2  48104  pgnbgreunbgrlem4  48106  pgnbgreunbgrlem5  48110  pgnbgreunbgr  48112  pgn4cyclex  48113  glbprlem  48950  toslat  48967