Theorem prcom 4686

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

Syntax hints:   = wceq 1541   ∪ cun 3896  {csn 4577  {cpr 4579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-un 3903  df-pr 4580

This theorem is referenced by:  preq2  4688  tpcoma  4704  tpidm23  4711  prid2g  4715  prid2  4717  prprc2  4720  difprsn2  4754  tpprceq3  4757  tppreqb  4758  ssprsseq  4778  preq2b  4800  preqr2  4802  preq12b  4803  prnebg  4809  preq12nebg  4816  opthprneg  4818  elpreqpr  4820  elpr2elpr  4822  fvpr2g  7134  en2other2  9911  hashprb  14311  joincomALT  18313  meetcomALT  18315  symggen  19390  psgnran  19435  lspprid2  20940  lspexchn2  21077  lspindp2l  21080  lspindp2  21081  lsppratlem1  21093  psgnghm  21526  uvcvvcl  21733  mdetralt  22543  mdetunilem7  22553  uhgr2edg  29207  usgredg4  29216  usgredg2vlem1  29224  usgredg2vlem2  29225  nbupgrel  29344  nbgr2vtx1edg  29349  nbuhgr2vtx1edgblem  29350  nbuhgr2vtx1edgb  29351  nbusgreledg  29352  nbgrssvwo2  29361  nbgrsym  29362  usgrnbcnvfv  29364  edgnbusgreu  29366  nbusgrf1o0  29368  nb3grprlem1  29379  nb3grprlem2  29380  nb3grpr  29381  nb3grpr2  29382  nb3gr2nb  29383  isuvtx  29394  cusgredg  29423  usgredgsscusgredg  29459  1hegrvtxdg1r  29508  1egrvtxdg1r  29510  vdegp1ci  29538  usgr2wlkneq  29755  usgr2trlncl  29759  usgr2pthlem  29762  uspgrn2crct  29807  2wlkdlem6  29930  umgr2adedgspth  29947  wwlks2onsym  29959  clwwlkn2  30045  clwwlknonex2  30110  wlk2v2elem2  30157  uhgr3cyclexlem  30182  umgr3cyclex  30184  frcond1  30267  frcond3  30270  frgr3v  30276  3vfriswmgr  30279  1to3vfriswmgr  30281  1to3vfriendship  30282  2pthfrgrrn  30283  3cyclfrgrrn1  30286  4cycl2v2nb  30290  n4cyclfrgr  30292  frgrnbnb  30294  frgrncvvdeqlem3  30302  frgrncvvdeqlem6  30305  frgrwopregbsn  30318  frgrwopreglem5ALT  30323  fusgr2wsp2nb  30335  2clwwlk2clwwlklem  30347  indf  32862  indpreima  32875  indsupp  32877  pmtrprfv2  33098  cyc3genpmlem  33161  measxun2  34295  measssd  34300  revwlk  35241  cusgr3cyclex  35252  2cycl2d  35255  poimirlem9  37742  poimirlem15  37748  dihprrn  41598  dvh3dim  41618  dvh3dim3N  41621  lcfrlem21  41735  mapdindp4  41895  mapdh6eN  41912  mapdh7dN  41922  mapdh8ab  41949  mapdh8ad  41951  mapdh8b  41952  mapdh8e  41956  hdmap1l6e  41986  hdmap11lem2  42014  sprsymrelf  47657  paireqne  47673  reuopreuprim  47688  dfodd5  47822  clnbupgrel  47996  clnbgrsym  48000  grtriproplem  48101  grtrif1o  48104  grtriclwlk3  48107  cycl3grtrilem  48108  usgrgrtrirex  48112  isubgr3stgrlem6  48133  isubgr3stgrlem7  48134  grlimprclnbgr  48158  grlimprclnbgrvtx  48161  usgrexmpl2nb1  48194  usgrexmpl2nb2  48195  usgrexmpl2nb3  48196  usgrexmpl2nb4  48197  usgrexmpl2nb5  48198  gpgprismgriedgdmss  48214  gpgedgvtx0  48223  gpgedgvtx1  48224  gpgedg2ov  48228  gpgedg2iv  48229  gpg5nbgrvtx03starlem3  48232  gpg5nbgrvtx03star  48242  gpg5nbgr3star  48243  gpgprismgr4cycllem3  48259  gpgprismgr4cycllem8  48264  pgnbgreunbgrlem1  48275  pgnbgreunbgrlem2lem3  48278  pgnbgreunbgrlem2  48279  pgnbgreunbgrlem4  48281  pgnbgreunbgrlem5  48285  pgnbgreunbgr  48287  pgn4cyclex  48288  glbprlem  49126  toslat  49143