Theorem prcom 3746

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

Syntax hints:   = wceq 1397   ∪ cun 3197  {csn 3668  {cpr 3669

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2212

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-v 2803  df-un 3203  df-pr 3675

This theorem is referenced by:  preq2  3748  tpcoma  3764  tpidm23  3771  prid2g  3775  prid2  3777  prprc2  3780  difprsn2  3812  ssprsseq  3834  preqr2g  3849  preqr2  3851  preq12b  3852  elpr2elpr  3858  fvpr2  5859  fvpr2g  5861  pr2cv2  7403  en2other2  7409  maxcom  11783  mincom  11809  xrmax2sup  11834  xrmaxltsup  11838  xrmaxadd  11841  xrbdtri  11856  lspprid2  14447  qtopbasss  15271  uhgr2edg  16083  usgredg4  16092  usgredg2vlem1  16099  usgredg2vlem2  16100  1hegrvtxdg1rfi  16187  vdegp1cid  16193  clwwlkn2  16298  clwwlknonex2  16316