Definition df-pr 4591

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

This definition is used by:  dfsn2  4601  dfpr2  4609  ralprgf  4659  rexprgf  4660  ralprg  4661  csbprg  4674  disjpr2  4678  prcom  4697  preq1  4698  qdass  4718  qdassr  4719  tpidm12  4720  prprc1  4730  difprsn1  4767  difpr  4770  tpprceq3  4771  snsspr1  4779  snsspr2  4780  prssg  4784  ssunpr  4798  sstp  4800  iunxprg  5061  iunopeqop  5503  iunopeqopOLD  5504  pwssun  5552  xpsspw  5795  dmpropg  6215  rnpropg  6222  funprg  6590  funtp  6593  fntpg  6596  funcnvpr  6598  f1oprswap  6866  f1oprg  6867  fnimapr  6964  xpprsng  7136  residpr  7139  fpr  7151  fmptpr  7170  fvpr1g  7188  f1ofvswap  7304  df2o3  8459  map2xp  9133  en2  9238  prfiALT  9282  prwf  9781  rankprb  9821  xp2dju  10167  ssxr  11285  prunioo  13514  prinfzo0  13734  fzosplitpr  13813  hashprg  14438  hashprlei  14512  s2prop  14951  s4prop  14954  f1oun2prg  14961  s2rn  15007  sumpr  15806  strle2  17225  phlstr  17405  symg2bas  19469  gsumpr  20031  dmdprdpr  20127  dprdpr  20128  lsmpr  21221  lsppr  21225  lspsntri  21229  lsppratlem1  21282  lsppratlem3  21284  lsppratlem4  21285  m2detleib  22799  xpstopnlem1  23977  ovolioo  25738  uniiccdif  25748  i1f1  25860  wilthlem2  27244  perfectlem2  27405  bdaypw2n0bndlem  28667  axlowdimlem13  29315  ex-dif  30785  ex-un  30786  ex-in  30787  ex-xp  30798  ex-cnv  30799  ex-rn  30802  ex-res  30803  spanpr  31943  superpos  32717  cnvprop  33052  brprop  33053  mptprop  33054  coprprop  33055  prct  33069  prodpr  33181  ccfldextdgrr  34071  esumpr  34465  eulerpartgbij  34771  signswch  34957  prodfzo03  34999  subfacp1lem1  35679  altopthsn  36461  onint1  36988  bj-prexg  37703  bj-prex  37704  bj-prfromadj  37709  poimirlem8  38307  poimirlem9  38308  poimirlem15  38314  smprngopr  38731  dihprrnlem1N  42226  dihprrnlem2  42227  djhlsmat  42229  lclkrlem2c  42311  lclkrlem2v  42330  lcfrlem18  42362  pr2dom  44281  dfrcl4  44430  iunrelexp0  44456  corclrcl  44461  corcltrcl  44493  cotrclrcl  44496  mnuprdlem2  45011  sumpair  45783  rnfdmpr  48046  perfectALTVlem2  48515  usgrexmpl2edg  48822  smprngprmrng  49132