Definition df-pr 4586

Description: Define unordered pair of classes. Definition 7.1 of [Quine] p. 48. For example, 𝐴 ∈ {1, -1} → (𝐴↑2) = 1 (ex-pr 30964). They are unordered, so {𝐴, 𝐵} = {𝐵, 𝐴} as proven by prcom 4692. For a more traditional definition, but requiring a dummy variable, see dfpr2 4604. {𝐴, 𝐴} is also an unordered pair, but also a singleton because of {𝐴} = {𝐴, 𝐴} (see dfsn2 4596). Therefore, {𝐴, 𝐵} is called a proper (unordered) pair iff 𝐴 ≠ 𝐵 and 𝐴 and 𝐵 are sets.

Note: ordered pairs are a completely different object defined below in df-op 4590. When the term "pair" is used without qualifier, it generally means "unordered pair", and the context makes it clear which version is meant. (Contributed by NM, 21-Jun-1993.)

Assertion

Ref	Expression
df-pr	⊢ {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})

Detailed syntax breakdown of Definition df-pr

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3	1, 2	cpr 4585	. 2 class {𝐴, 𝐵}
4	1	csn 4583	. . 3 class {𝐴}
5	2	csn 4583	. . 3 class {𝐵}
6	4, 5	cun 3896	. 2 class ({𝐴} ∪ {𝐵})
7	3, 6	wceq 1570	1 wff {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})

This definition is used by:  dfsn2  4596  dfpr2  4604  ralprgf  4654  rexprgf  4655  ralprg  4656  csbprg  4669  disjpr2  4673  prcom  4692  preq1  4693  qdass  4713  qdassr  4714  tpidm12  4715  prprc1  4725  difprsn1  4762  difpr  4765  tpprceq3  4766  snsspr1  4774  snsspr2  4775  prssg  4779  ssunpr  4793  sstp  4795  iunxprg  5055  iunopeqop  5490  iunopeqopOLD  5491  pwssun  5539  xpsspw  5783  dmpropg  6205  rnpropg  6212  funprg  6582  funtp  6585  fntpg  6588  funcnvpr  6590  f1oprswap  6858  f1oprg  6859  fnimapr  6956  xpprsng  7130  xpsnprg  7131  xpsntpg  7132  residpr  7134  fpr  7146  fmptpr  7165  fvpr1g  7183  f1ofvswap  7302  df2o3  8462  map2xp  9144  en2  9249  prfiALT  9294  prwf  9793  rankprb  9838  xp2dju  10226  ssxr  11350  prunioo  13581  prinfzo0  13801  fzosplitpr  13880  hashprg  14506  hashprlei  14580  s2prop  15025  s4prop  15028  f1oun2prg  15035  s2rn  15083  sumpr  15881  strle2  17298  phlstr  17478  symg2bas  19568  gsumpr  20130  dmdprdpr  20226  dprdpr  20227  lsmpr  21325  lsppr  21329  lspsntri  21333  lsppratlem1  21386  lsppratlem3  21388  lsppratlem4  21389  m2detleib  22907  xpstopnlem1  24089  ovolioo  25850  uniiccdif  25860  i1f1  25972  wilthlem2  27359  perfectlem2  27520  bdaypw2n0bndlem  28782  axlowdimlem13  29465  ex-dif  30957  ex-un  30958  ex-in  30959  ex-xp  30970  ex-cnv  30971  ex-rn  30974  ex-res  30975  spanpr  32115  superpos  32889  cnvprop  33222  brprop  33223  mptprop  33224  coprprop  33225  prct  33239  prodpr  33350  ccfldextdgrr  34237  esumpr  34631  eulerpartgbij  34938  signswch  35124  prodfzo03  35166  subfacp1lem1  35865  altopthsn  36648  onint1  37159  bj-prexg  37874  bj-prex  37875  bj-prfromadj  37880  poimirlem8  38466  poimirlem9  38467  poimirlem15  38473  smprngopr  38906  dihprrnlem1N  42401  dihprrnlem2  42402  djhlsmat  42404  lclkrlem2c  42486  lclkrlem2v  42505  lcfrlem18  42537  pr2dom  44471  dfrcl4  44620  iunrelexp0  44646  corclrcl  44651  corcltrcl  44683  cotrclrcl  44686  mnuprdlem2  45201  sumpair  45973  rnfdmpr  48273  perfectALTVlem2  48742  usgrexmpl2edg  49049  smprngprmrng  49358