Definition df-pr 4591

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

This definition is referenced by:  dfsn2  4601  dfpr2  4609  ralprgf  4659  rexprgf  4660  ralprg  4661  csbprg  4674  disjpr2  4678  prcom  4697  preq1  4698  qdass  4718  qdassr  4719  tpidm12  4720  prprc1  4730  difprsn1  4767  difpr  4770  tpprceq3  4771  snsspr1  4779  snsspr2  4780  prssg  4784  ssunpr  4798  sstp  4800  iunxprg  5061  iunopeqop  5504  iunopeqopOLD  5505  pwssun  5553  xpsspw  5796  dmpropg  6216  rnpropg  6223  funprg  6590  funtp  6593  fntpg  6596  funcnvpr  6598  f1oprswap  6866  f1oprg  6867  fnimapr  6964  xpprsng  7136  residpr  7139  fpr  7151  fmptpr  7170  fvpr1g  7188  f1ofvswap  7304  df2o3  8460  map2xp  9134  en2  9239  prfiALT  9283  prwf  9782  rankprb  9822  xp2dju  10159  ssxr  11278  prunioo  13507  prinfzo0  13726  fzosplitpr  13805  hashprg  14430  hashprlei  14504  s2prop  14943  s4prop  14946  f1oun2prg  14953  s2rn  14999  sumpr  15798  strle2  17218  phlstr  17398  symg2bas  19462  gsumpr  20024  dmdprdpr  20120  dprdpr  20121  lsmpr  21189  lsppr  21193  lspsntri  21197  lsppratlem1  21250  lsppratlem3  21252  lsppratlem4  21253  m2detleib  22767  xpstopnlem1  23945  ovolioo  25706  uniiccdif  25716  i1f1  25828  wilthlem2  27209  perfectlem2  27370  bdaypw2n0bndlem  28632  axlowdimlem13  29270  ex-dif  30740  ex-un  30741  ex-in  30742  ex-xp  30753  ex-cnv  30754  ex-rn  30757  ex-res  30758  spanpr  31898  superpos  32672  cnvprop  33007  brprop  33008  mptprop  33009  coprprop  33010  prct  33024  prodpr  33136  ccfldextdgrr  34028  esumpr  34422  eulerpartgbij  34728  signswch  34914  prodfzo03  34956  subfacp1lem1  35625  altopthsn  36407  onint1  36904  bj-prexg  37619  bj-prex  37620  bj-prfromadj  37625  poimirlem8  38223  poimirlem9  38224  poimirlem15  38230  smprngopr  38647  dihprrnlem1N  42144  dihprrnlem2  42145  djhlsmat  42147  lclkrlem2c  42229  lclkrlem2v  42248  lcfrlem18  42280  pr2dom  44201  dfrcl4  44350  iunrelexp0  44376  corclrcl  44381  corcltrcl  44413  cotrclrcl  44416  mnuprdlem2  44931  sumpair  45703  rnfdmpr  47963  perfectALTVlem2  48432  usgrexmpl2edg  48739  smprngprmrng  49049