Definition df-pr 4632

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

This definition is referenced by:  dfsn2  4642  dfpr2  4648  ralprgf  4697  rexprgf  4698  ralprg  4699  csbprg  4714  disjpr2  4718  prcom  4737  preq1  4738  qdass  4758  qdassr  4759  tpidm12  4760  prprc1  4770  difprsn1  4804  difpr  4807  tpprceq3  4808  snsspr1  4818  snsspr2  4819  prssg  4823  ssunpr  4836  sstp  4838  iunxprg  5100  iunopeqop  5522  pwssun  5572  xpsspw  5810  dmpropg  6215  rnpropg  6222  funprg  6603  funtp  6606  fntpg  6609  funcnvpr  6611  f1oprswap  6878  f1oprg  6879  fnimapr  6976  xpprsng  7141  residpr  7144  fpr  7155  fmptpr  7173  fvpr1g  7191  fvpr2gOLD  7193  fvpr1OLD  7195  f1ofvswap  7308  df2o3  8478  enpr2dOLD  9054  map2xp  9151  1sdomOLD  9253  en2  9285  prfi  9326  prwf  9810  rankprb  9850  pr2nelemOLD  10002  xp2dju  10175  ssxr  11289  prunioo  13464  prinfzo0  13677  fzosplitpr  13747  hashprg  14361  hashprlei  14435  s2prop  14864  s4prop  14867  f1oun2prg  14874  sumpr  15700  strle2  17098  phlstr  17297  symg2bas  19303  gsumpr  19866  dmdprdpr  19962  dprdpr  19963  lsmpr  20846  lsppr  20850  lspsntri  20854  lsppratlem1  20907  lsppratlem3  20909  lsppratlem4  20910  m2detleib  22355  xpstopnlem1  23535  ovolioo  25319  uniiccdif  25329  i1f1  25441  wilthlem2  26807  perfectlem2  26967  axlowdimlem13  28477  ex-dif  29941  ex-un  29942  ex-in  29943  ex-xp  29954  ex-cnv  29955  ex-rn  29958  ex-res  29959  spanpr  31098  superpos  31872  cnvprop  32183  brprop  32184  mptprop  32185  coprprop  32186  prct  32204  prodpr  32297  ccfldextdgrr  33033  esumpr  33360  eulerpartgbij  33667  signswch  33868  prodfzo03  33911  subfacp1lem1  34466  altopthsn  35235  onint1  35639  bj-prexg  36225  bj-prex  36226  bj-prfromadj  36231  poimirlem8  36801  poimirlem9  36802  poimirlem15  36808  smprngopr  37225  dihprrnlem1N  40600  dihprrnlem2  40601  djhlsmat  40603  lclkrlem2c  40685  lclkrlem2v  40704  lcfrlem18  40736  pr2dom  42582  dfrcl4  42731  iunrelexp0  42757  corclrcl  42762  corcltrcl  42794  cotrclrcl  42797  mnuprdlem2  43336  sumpair  44023  rnfdmpr  46289  perfectALTVlem2  46690