Theorem prcom 4693

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

This proof depends on syntax axioms:   = wceq 1570   ∪ cun 3897  {csn 4584  {cpr 4586

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3904  df-pr 4587

This theorem is used by:  preq2  4695  tpcoma  4711  tpidm23  4718  prid2g  4722  prid2  4724  prprc2  4727  difprsn2  4764  tpprceq3  4767  tppreqb  4768  ssprsseq  4786  preq2b  4807  preqr2  4809  preq12b  4810  prnebg  4816  preq12nebg  4823  opthprneg  4825  elpreqpr  4827  elpr2elpr  4829  fvpr2g  7190  en2other2  10015  indf  12251  hashprb  14464  joincomALT  18490  meetcomALT  18492  symggen  19600  psgnran  19645  lspprid2  21185  lspexchn2  21321  lspindp2l  21324  lspindp2  21325  lsppratlem1  21337  psgnghm  21796  uvcvvcl  22003  mdetralt  22833  mdetunilem7  22843  uhgr2edg  29671  usgredg4  29680  usgredg2vlem1  29688  usgredg2vlem2  29689  nbupgrel  29808  nbgr2vtx1edg  29813  nbuhgr2vtx1edgblem  29814  nbuhgr2vtx1edgb  29815  nbusgreledg  29816  nbgrssvwo2  29825  nbgrsym  29826  usgrnbcnvfv  29828  edgnbusgreu  29830  nbusgrf1o0  29832  nb3grprlem1  29843  nb3grprlem2  29844  nb3grpr  29845  nb3grpr2  29846  nb3gr2nb  29847  isuvtx  29858  cusgredg  29887  usgredgsscusgredg  29922  1hegrvtxdg1r  29971  1egrvtxdg1r  29973  vdegp1ci  30001  revwlk  30149  usgr2wlkneq  30224  usgr2trlncl  30228  usgr2pthlem  30231  uspgrn2crct  30279  2wlkdlem6  30402  umgr2adedgspth  30419  wwlks2onsym  30431  clwwlkn2  30517  clwwlknonex2  30582  umgr2cycllem  30628  wlk2v2elem2  30639  uhgr3cyclexlem  30664  umgr3cyclex  30666  frcond1  30749  frcond3  30752  frgr3v  30758  3vfriswmgr  30761  1to3vfriswmgr  30763  1to3vfriendship  30764  2pthfrgrrn  30765  3cyclfrgrrn1  30768  4cycl2v2nb  30772  n4cyclfrgr  30774  frgrnbnb  30776  frgrncvvdeqlem3  30784  frgrncvvdeqlem6  30787  frgrwopregbsn  30800  frgrwopreglem5ALT  30805  fusgr2wsp2nb  30817  2clwwlk2clwwlklem  30829  indpreima  33314  indsupp  33316  pmtrprfv2  33531  cyc3genpmlem  33594  measxun2  34724  measssd  34729  cusgr3cyclex  35728  2cycl2d  35729  poimirlem9  38381  poimirlem15  38387  dihprrn  42302  dvh3dim  42322  dvh3dim3N  42325  lcfrlem21  42439  mapdindp4  42599  mapdh6eN  42616  mapdh7dN  42626  mapdh8ab  42653  mapdh8ad  42655  mapdh8b  42656  mapdh8e  42660  hdmap1l6e  42690  hdmap11lem2  42718  sprsymrelf  48398  paireqne  48414  reuopreuprim  48429  dfodd5  48579  clnbupgrel  48753  clnbgrsym  48757  grtriproplem  48858  grtrif1o  48861  grtriclwlk3  48864  cycl3grtrilem  48865  usgrgrtrirex  48869  isubgr3stgrlem6  48890  isubgr3stgrlem7  48891  grlimprclnbgr  48915  grlimprclnbgrvtx  48918  usgrexmpl2nb1  48951  usgrexmpl2nb2  48952  usgrexmpl2nb3  48953  usgrexmpl2nb4  48954  usgrexmpl2nb5  48955  gpgprismgriedgdmss  48971  gpgedgvtx0  48980  gpgedgvtx1  48981  gpgedg2ov  48985  gpgedg2iv  48986  gpg5nbgrvtx03starlem3  48989  gpg5nbgrvtx03star  48999  gpg5nbgr3star  49000  gpgprismgr4cycllem3  49016  gpgprismgr4cycllem8  49021  pgnbgreunbgrlem1  49032  pgnbgreunbgrlem2lem3  49035  pgnbgreunbgrlem2  49036  pgnbgreunbgrlem4  49038  pgnbgreunbgrlem5  49042  pgnbgreunbgr  49044  pgn4cyclex  49045  glbprlem  49894  toslat  49911