Definition df-pr 4565

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

This definition is referenced by:  dfsn2  4575  dfpr2  4581  ralprgf  4629  rexprgf  4630  ralprg  4631  csbprg  4646  disjpr2  4650  prcom  4669  preq1  4670  qdass  4690  qdassr  4691  tpidm12  4692  prprc1  4702  difprsn1  4734  difpr  4737  tpprceq3  4738  snsspr1  4748  snsspr2  4749  prssg  4753  ssunpr  4766  sstp  4768  iunxprg  5026  iunopeqop  5436  pwssun  5486  xpsspw  5721  dmpropg  6123  rnpropg  6130  funprg  6495  funtp  6498  fntpg  6501  funcnvpr  6503  f1oprswap  6769  f1oprg  6770  fnimapr  6861  xpprsng  7021  residpr  7024  fpr  7035  fmptpr  7053  fvpr1g  7071  fvpr2gOLD  7073  fvpr1OLD  7075  f1ofvswap  7187  df2o3  8314  enpr2d  8847  map2xp  8943  1sdom  9034  en2  9062  prfi  9098  prwf  9578  rankprb  9618  pr2nelem  9769  xp2dju  9941  ssxr  11053  prunioo  13222  prinfzo0  13435  fzosplitpr  13505  hashprg  14119  hashprlei  14191  s2prop  14629  s4prop  14632  f1oun2prg  14639  sumpr  15469  strle2  16869  phlstr  17065  symg2bas  19009  gsumpr  19565  dmdprdpr  19661  dprdpr  19662  lsmpr  20360  lsppr  20364  lspsntri  20368  lsppratlem1  20418  lsppratlem3  20420  lsppratlem4  20421  m2detleib  21789  xpstopnlem1  22969  ovolioo  24741  uniiccdif  24751  i1f1  24863  wilthlem2  26227  perfectlem2  26387  axlowdimlem13  27331  ex-dif  28796  ex-un  28797  ex-in  28798  ex-xp  28809  ex-cnv  28810  ex-rn  28813  ex-res  28814  spanpr  29951  superpos  30725  cnvprop  31038  brprop  31039  mptprop  31040  coprprop  31041  prct  31058  prodpr  31149  ccfldextdgrr  31751  esumpr  32043  eulerpartgbij  32348  signswch  32549  prodfzo03  32592  subfacp1lem1  33150  altopthsn  34272  onint1  34647  poimirlem8  35794  poimirlem9  35795  poimirlem15  35801  smprngopr  36219  dihprrnlem1N  39445  dihprrnlem2  39446  djhlsmat  39448  lclkrlem2c  39530  lclkrlem2v  39549  lcfrlem18  39581  pr2dom  41141  dfrcl4  41291  iunrelexp0  41317  corclrcl  41322  corcltrcl  41354  cotrclrcl  41357  mnuprdlem2  41898  sumpair  42585  rnfdmpr  44784  perfectALTVlem2  45185