Definition df-pr 4590

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

This definition is used by:  dfsn2  4600  dfpr2  4608  ralprgf  4658  rexprgf  4659  ralprg  4660  csbprg  4673  disjpr2  4677  prcom  4696  preq1  4697  qdass  4717  qdassr  4718  tpidm12  4719  prprc1  4729  difprsn1  4766  difpr  4769  tpprceq3  4770  snsspr1  4778  snsspr2  4779  prssg  4783  ssunpr  4797  sstp  4799  iunxprg  5060  iunopeqop  5502  iunopeqopOLD  5503  pwssun  5551  xpsspw  5794  dmpropg  6215  rnpropg  6222  funprg  6591  funtp  6594  fntpg  6597  funcnvpr  6599  f1oprswap  6867  f1oprg  6868  fnimapr  6965  xpprsng  7138  xpsnprg  7139  xpsntpg  7140  residpr  7142  fpr  7154  fmptpr  7173  fvpr1g  7191  f1ofvswap  7310  df2o3  8466  map2xp  9148  en2  9253  prfiALT  9297  prwf  9796  rankprb  9836  xp2dju  10182  ssxr  11306  prunioo  13536  prinfzo0  13756  fzosplitpr  13835  hashprg  14461  hashprlei  14535  s2prop  14980  s4prop  14983  f1oun2prg  14990  s2rn  15038  sumpr  15836  strle2  17255  phlstr  17435  symg2bas  19521  gsumpr  20083  dmdprdpr  20179  dprdpr  20180  lsmpr  21274  lsppr  21278  lspsntri  21282  lsppratlem1  21335  lsppratlem3  21337  lsppratlem4  21338  m2detleib  22854  xpstopnlem1  24036  ovolioo  25797  uniiccdif  25807  i1f1  25919  wilthlem2  27303  perfectlem2  27464  bdaypw2n0bndlem  28726  axlowdimlem13  29397  ex-dif  30889  ex-un  30890  ex-in  30891  ex-xp  30902  ex-cnv  30903  ex-rn  30906  ex-res  30907  spanpr  32047  superpos  32821  cnvprop  33155  brprop  33156  mptprop  33157  coprprop  33158  prct  33172  prodpr  33283  ccfldextdgrr  34169  esumpr  34563  eulerpartgbij  34870  signswch  35056  prodfzo03  35098  subfacp1lem1  35745  altopthsn  36528  onint1  37055  bj-prexg  37770  bj-prex  37771  bj-prfromadj  37776  poimirlem8  38364  poimirlem9  38365  poimirlem15  38371  smprngopr  38789  dihprrnlem1N  42284  dihprrnlem2  42285  djhlsmat  42287  lclkrlem2c  42369  lclkrlem2v  42388  lcfrlem18  42420  pr2dom  44354  dfrcl4  44503  iunrelexp0  44529  corclrcl  44534  corcltrcl  44566  cotrclrcl  44569  mnuprdlem2  45084  sumpair  45856  rnfdmpr  48156  perfectALTVlem2  48625  usgrexmpl2edg  48932  smprngprmrng  49241