Theorem prcom 3695

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

Syntax hints:   = wceq 1364   ∪ cun 3152  {csn 3619  {cpr 3620

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3158  df-pr 3626

This theorem is referenced by:  preq2  3697  tpcoma  3713  tpidm23  3720  prid2g  3724  prid2  3726  prprc2  3728  difprsn2  3759  preqr2g  3794  preqr2  3796  preq12b  3797  fvpr2  5764  fvpr2g  5766  en2other2  7258  maxcom  11350  mincom  11375  xrmax2sup  11400  xrmaxltsup  11404  xrmaxadd  11407  xrbdtri  11422  lspprid2  13911  qtopbasss  14700