Theorem prcom 3745

Description: Commutative law for unordered pairs. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
prcom	⊢ {𝐴, 𝐵} = {𝐵, 𝐴}

Proof of Theorem prcom

Step	Hyp	Ref	Expression
1		uncom 3349	. 2 ⊢ ({𝐴} ∪ {𝐵}) = ({𝐵} ∪ {𝐴})
2		df-pr 3674	. 2 ⊢ {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})
3		df-pr 3674	. 2 ⊢ {𝐵, 𝐴} = ({𝐵} ∪ {𝐴})
4	1, 2, 3	3eqtr4i 2260	1 ⊢ {𝐴, 𝐵} = {𝐵, 𝐴}

Syntax hints:   = wceq 1395   ∪ cun 3196  {csn 3667  {cpr 3668

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2802  df-un 3202  df-pr 3674

This theorem is referenced by:  preq2  3747  tpcoma  3763  tpidm23  3770  prid2g  3774  prid2  3776  prprc2  3779  difprsn2  3811  ssprsseq  3833  preqr2g  3848  preqr2  3850  preq12b  3851  elpr2elpr  3857  fvpr2  5854  fvpr2g  5856  pr2cv2  7392  en2other2  7397  maxcom  11754  mincom  11780  xrmax2sup  11805  xrmaxltsup  11809  xrmaxadd  11812  xrbdtri  11827  lspprid2  14416  qtopbasss  15235  uhgr2edg  16045  usgredg4  16054  usgredg2vlem1  16061  usgredg2vlem2  16062  clwwlkn2  16216  clwwlknonex2  16234