Definition df-pr 4560

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

This definition is referenced by:  dfsn2  4570  dfpr2  4578  ralprgf  4628  rexprgf  4629  ralprg  4630  csbprg  4643  disjpr2  4647  prcom  4666  preq1  4667  qdass  4687  qdassr  4688  tpidm12  4689  prprc1  4699  difprsn1  4735  difpr  4738  tpprceq3  4739  snsspr1  4747  snsspr2  4748  prssg  4752  ssunpr  4767  sstp  4769  iunxprg  5027  iunopeqop  5464  iunopeqopOLD  5465  pwssun  5512  xpsspw  5754  dmpropg  6169  rnpropg  6176  funprg  6542  funtp  6545  fntpg  6548  funcnvpr  6550  f1oprswap  6815  f1oprg  6816  fnimapr  6913  xpprsng  7085  residpr  7088  fpr  7100  fmptpr  7119  fvpr1g  7137  f1ofvswap  7253  df2o3  8407  map2xp  9079  en2  9184  prfiALT  9229  prwf  9730  rankprb  9770  xp2dju  10094  ssxr  11211  prunioo  13429  prinfzo0  13648  fzosplitpr  13727  hashprg  14352  hashprlei  14425  s2prop  14864  s4prop  14867  f1oun2prg  14874  s2rn  14920  sumpr  15705  strle2  17124  phlstr  17304  symg2bas  19362  gsumpr  19924  dmdprdpr  20020  dprdpr  20021  lsmpr  21082  lsppr  21086  lspsntri  21090  lsppratlem1  21143  lsppratlem3  21145  lsppratlem4  21146  m2detleib  22617  xpstopnlem1  23795  ovolioo  25556  uniiccdif  25566  i1f1  25678  wilthlem2  27053  perfectlem2  27214  bdaypw2n0bndlem  28475  axlowdimlem13  29043  ex-dif  30513  ex-un  30514  ex-in  30515  ex-xp  30526  ex-cnv  30527  ex-rn  30530  ex-res  30531  spanpr  31671  superpos  32445  cnvprop  32790  brprop  32791  mptprop  32792  coprprop  32793  prct  32807  prodpr  32920  ccfldextdgrr  33866  esumpr  34260  eulerpartgbij  34566  signswch  34755  prodfzo03  34797  subfacp1lem1  35420  altopthsn  36202  onint1  36690  bj-prexg  37405  bj-prex  37406  bj-prfromadj  37411  poimirlem8  38008  poimirlem9  38009  poimirlem15  38015  smprngopr  38432  dihprrnlem1N  41929  dihprrnlem2  41930  djhlsmat  41932  lclkrlem2c  42014  lclkrlem2v  42033  lcfrlem18  42065  pr2dom  43984  dfrcl4  44133  iunrelexp0  44159  corclrcl  44164  corcltrcl  44196  cotrclrcl  44199  mnuprdlem2  44730  sumpair  45496  rnfdmpr  47756  perfectALTVlem2  48225  usgrexmpl2edg  48532