ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  prcom GIF version

Theorem prcom 3513
Description: Commutative law for unordered pairs. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
prcom {𝐴, 𝐵} = {𝐵, 𝐴}

Proof of Theorem prcom
StepHypRef Expression
1 uncom 3142 . 2 ({𝐴} ∪ {𝐵}) = ({𝐵} ∪ {𝐴})
2 df-pr 3448 . 2 {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})
3 df-pr 3448 . 2 {𝐵, 𝐴} = ({𝐵} ∪ {𝐴})
41, 2, 33eqtr4i 2118 1 {𝐴, 𝐵} = {𝐵, 𝐴}
Colors of variables: wff set class
Syntax hints:   = wceq 1289  cun 2995  {csn 3441  {cpr 3442
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-v 2621  df-un 3001  df-pr 3448
This theorem is referenced by:  preq2  3515  tpcoma  3531  tpidm23  3538  prid2g  3542  prid2  3544  prprc2  3546  difprsn2  3572  preqr2g  3606  preqr2  3608  preq12b  3609  fvpr2  5484  fvpr2g  5486  en2other2  6801  maxcom  10601  mincom  10624
  Copyright terms: Public domain W3C validator