Definition df-pr 4584

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

This definition is referenced by:  dfsn2  4594  dfpr2  4602  ralprgf  4652  rexprgf  4653  ralprg  4654  csbprg  4667  disjpr2  4671  prcom  4690  preq1  4691  qdass  4711  qdassr  4712  tpidm12  4713  prprc1  4723  difprsn1  4757  difpr  4760  tpprceq3  4761  snsspr1  4771  snsspr2  4772  prssg  4776  ssunpr  4791  sstp  4793  iunxprg  5052  iunopeqop  5470  pwssun  5517  xpsspw  5759  dmpropg  6174  rnpropg  6181  funprg  6547  funtp  6550  fntpg  6553  funcnvpr  6555  f1oprswap  6820  f1oprg  6821  fnimapr  6918  xpprsng  7087  residpr  7090  fpr  7101  fmptpr  7120  fvpr1g  7138  f1ofvswap  7254  df2o3  8407  map2xp  9079  en2  9184  prfiALT  9229  prwf  9727  rankprb  9767  xp2dju  10091  ssxr  11206  prunioo  13401  prinfzo0  13618  fzosplitpr  13697  hashprg  14322  hashprlei  14395  s2prop  14834  s4prop  14837  f1oun2prg  14844  s2rn  14890  sumpr  15675  strle2  17090  phlstr  17270  symg2bas  19326  gsumpr  19888  dmdprdpr  19984  dprdpr  19985  lsmpr  21045  lsppr  21049  lspsntri  21053  lsppratlem1  21106  lsppratlem3  21108  lsppratlem4  21109  m2detleib  22579  xpstopnlem1  23757  ovolioo  25529  uniiccdif  25539  i1f1  25651  wilthlem2  27039  perfectlem2  27201  bdaypw2n0bndlem  28463  axlowdimlem13  29031  ex-dif  30502  ex-un  30503  ex-in  30504  ex-xp  30515  ex-cnv  30516  ex-rn  30519  ex-res  30520  spanpr  31659  superpos  32433  cnvprop  32777  brprop  32778  mptprop  32779  coprprop  32780  prct  32794  prodpr  32909  ccfldextdgrr  33831  esumpr  34225  eulerpartgbij  34531  signswch  34720  prodfzo03  34762  subfacp1lem1  35375  altopthsn  36157  onint1  36645  bj-prexg  37242  bj-prex  37243  bj-prfromadj  37248  poimirlem8  37831  poimirlem9  37832  poimirlem15  37838  smprngopr  38255  dihprrnlem1N  41752  dihprrnlem2  41753  djhlsmat  41755  lclkrlem2c  41837  lclkrlem2v  41856  lcfrlem18  41888  pr2dom  43835  dfrcl4  43984  iunrelexp0  44010  corclrcl  44015  corcltrcl  44047  cotrclrcl  44050  mnuprdlem2  44581  sumpair  45347  rnfdmpr  47594  perfectALTVlem2  48035  usgrexmpl2edg  48342