Definition df-pr 4576

Description: Define unordered pair of classes. Definition 7.1 of [Quine] p. 48. For example, 𝐴 ∈ {1, -1} → (𝐴↑2) = 1 (ex-pr 30410). They are unordered, so {𝐴, 𝐵} = {𝐵, 𝐴} as proven by prcom 4682. For a more traditional definition, but requiring a dummy variable, see dfpr2 4594. {𝐴, 𝐴} is also an unordered pair, but also a singleton because of {𝐴} = {𝐴, 𝐴} (see dfsn2 4586). 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 4580. 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 4575	. 2 class {𝐴, 𝐵}
4	1	csn 4573	. . 3 class {𝐴}
5	2	csn 4573	. . 3 class {𝐵}
6	4, 5	cun 3895	. 2 class ({𝐴} ∪ {𝐵})
7	3, 6	wceq 1541	1 wff {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})

This definition is referenced by:  dfsn2  4586  dfpr2  4594  ralprgf  4644  rexprgf  4645  ralprg  4646  csbprg  4659  disjpr2  4663  prcom  4682  preq1  4683  qdass  4703  qdassr  4704  tpidm12  4705  prprc1  4715  difprsn1  4749  difpr  4752  tpprceq3  4753  snsspr1  4763  snsspr2  4764  prssg  4768  ssunpr  4783  sstp  4785  iunxprg  5042  iunopeqop  5459  pwssun  5506  xpsspw  5748  dmpropg  6162  rnpropg  6169  funprg  6535  funtp  6538  fntpg  6541  funcnvpr  6543  f1oprswap  6807  f1oprg  6808  fnimapr  6905  xpprsng  7073  residpr  7076  fpr  7087  fmptpr  7106  fvpr1g  7124  f1ofvswap  7240  df2o3  8393  map2xp  9060  en2  9164  prfiALT  9209  prwf  9704  rankprb  9744  xp2dju  10068  ssxr  11182  prunioo  13381  prinfzo0  13598  fzosplitpr  13677  hashprg  14302  hashprlei  14375  s2prop  14814  s4prop  14817  f1oun2prg  14824  s2rn  14870  sumpr  15655  strle2  17070  phlstr  17250  symg2bas  19305  gsumpr  19867  dmdprdpr  19963  dprdpr  19964  lsmpr  21023  lsppr  21027  lspsntri  21031  lsppratlem1  21084  lsppratlem3  21086  lsppratlem4  21087  m2detleib  22546  xpstopnlem1  23724  ovolioo  25496  uniiccdif  25506  i1f1  25618  wilthlem2  27006  perfectlem2  27168  axlowdimlem13  28932  ex-dif  30403  ex-un  30404  ex-in  30405  ex-xp  30416  ex-cnv  30417  ex-rn  30420  ex-res  30421  spanpr  31560  superpos  32334  cnvprop  32677  brprop  32678  mptprop  32679  coprprop  32680  prct  32696  prodpr  32809  ccfldextdgrr  33685  esumpr  34079  eulerpartgbij  34385  signswch  34574  prodfzo03  34616  subfacp1lem1  35223  altopthsn  36005  onint1  36493  bj-prexg  37083  bj-prex  37084  bj-prfromadj  37089  poimirlem8  37678  poimirlem9  37679  poimirlem15  37685  smprngopr  38102  dihprrnlem1N  41533  dihprrnlem2  41534  djhlsmat  41536  lclkrlem2c  41618  lclkrlem2v  41637  lcfrlem18  41669  pr2dom  43630  dfrcl4  43779  iunrelexp0  43805  corclrcl  43810  corcltrcl  43842  cotrclrcl  43845  mnuprdlem2  44376  sumpair  45142  rnfdmpr  47391  perfectALTVlem2  47832  usgrexmpl2edg  48139