MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-pr Structured version   Visualization version   GIF version

Definition df-pr 4158
Description: Define unordered pair of classes. Definition 7.1 of [Quine] p. 48. For example, 𝐴 ∈ {1, -1} → (𝐴↑2) = 1 (ex-pr 27175). They are unordered, so {𝐴, 𝐵} = {𝐵, 𝐴} as proven by prcom 4244. For a more traditional definition, but requiring a dummy variable, see dfpr2 4173. (Contributed by NM, 21-Jun-1993.)
Assertion
Ref Expression
df-pr {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})

Detailed syntax breakdown of Definition df-pr
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
31, 2cpr 4157 . 2 class {𝐴, 𝐵}
41csn 4155 . . 3 class {𝐴}
52csn 4155 . . 3 class {𝐵}
64, 5cun 3558 . 2 class ({𝐴} ∪ {𝐵})
73, 6wceq 1480 1 wff {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})
Colors of variables: wff setvar class
This definition is referenced by:  dfsn2  4168  dfpr2  4173  ralprg  4212  rexprg  4213  csbprg  4222  disjpr2  4225  disjpr2OLD  4226  prcom  4244  preq1  4245  qdass  4265  qdassr  4266  tpidm12  4267  prprc1  4277  difprsn1  4306  diftpsn3OLD  4309  difpr  4310  tpprceq3  4311  snsspr1  4320  snsspr2  4321  prssg  4325  prssOLD  4327  ssunpr  4340  sstp  4342  iunxprg  4580  iunopeqop  4951  pwssun  4990  xpsspw  5204  dmpropg  5577  rnpropg  5584  funprg  5908  funprgOLD  5909  funtp  5913  fntpg  5916  funcnvpr  5918  f1oprswap  6147  f1oprg  6148  fnimapr  6229  residpr  6374  fpr  6386  fmptpr  6403  fvpr1  6421  fvpr1g  6423  fvpr2g  6424  df2o3  7533  map2xp  8090  1sdom  8123  en2  8156  prfi  8195  prwf  8634  rankprb  8674  pr2nelem  8787  xp2cda  8962  ssxr  10067  prunioo  12259  prinfzo0  12463  fzosplitprm1  12534  hashprg  13138  hashprgOLD  13139  hashprlei  13204  s2prop  13604  s4prop  13607  f1oun2prg  13614  sumpr  14426  isprm2lem  15337  strlemor2OLD  15910  strle2  15914  phlstr  15974  xpscg  16158  symg2bas  17758  dmdprdpr  18388  dprdpr  18389  lsmpr  19029  lsppr  19033  lspsntri  19037  lsppratlem1  19087  lsppratlem3  19089  lsppratlem4  19090  m2detleib  20377  xpstopnlem1  21552  ovolioo  23276  uniiccdif  23286  i1f1  23397  wilthlem2  24729  perfectlem2  24889  axlowdimlem13  25768  ex-dif  27168  ex-un  27169  ex-in  27170  ex-xp  27181  ex-cnv  27182  ex-rn  27185  ex-res  27186  spanpr  28327  superpos  29101  prct  29376  esumpr  29951  eulerpartgbij  30257  signswch  30460  subfacp1lem1  30922  altopthsn  31763  onint1  32143  poimirlem8  33088  poimirlem9  33089  poimirlem15  33095  smprngopr  33522  dihprrnlem1N  36232  dihprrnlem2  36233  djhlsmat  36235  lclkrlem2c  36317  lclkrlem2v  36336  lcfrlem18  36368  dfrcl4  37488  iunrelexp0  37514  corclrcl  37519  corcltrcl  37551  cotrclrcl  37554  sumpair  38716  rnfdmpr  40627  fzosplitpr  40666  perfectALTVlem2  40956  xpprsng  41428  gsumpr  41457
  Copyright terms: Public domain W3C validator