Definition df-pr 4570

Description: Define unordered pair of classes. Definition 7.1 of [Quine] p. 48. For example, 𝐴 ∈ {1, -1} → (𝐴↑2) = 1 (ex-pr 28209). They are unordered, so {𝐴, 𝐵} = {𝐵, 𝐴} as proven by prcom 4668. For a more traditional definition, but requiring a dummy variable, see dfpr2 4586. {𝐴, 𝐴} is also an unordered pair, but also a singleton because of {𝐴} = {𝐴, 𝐴} (see dfsn2 4580). Therefore, {𝐴, 𝐵} is called a proper (unordered) pair iff 𝐴 ≠ 𝐵 and 𝐴 and 𝐵 are sets. (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 4569	. 2 class {𝐴, 𝐵}
4	1	csn 4567	. . 3 class {𝐴}
5	2	csn 4567	. . 3 class {𝐵}
6	4, 5	cun 3934	. 2 class ({𝐴} ∪ {𝐵})
7	3, 6	wceq 1537	1 wff {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})

This definition is referenced by:  dfsn2  4580  dfpr2  4586  ralprgf  4630  rexprgf  4631  csbprg  4645  disjpr2  4649  prcom  4668  preq1  4669  qdass  4689  qdassr  4690  tpidm12  4691  prprc1  4701  difprsn1  4733  difpr  4736  tpprceq3  4737  snsspr1  4747  snsspr2  4748  prssg  4752  ssunpr  4765  sstp  4767  iunxprg  5018  iunopeqop  5411  pwssun  5456  xpsspw  5682  dmpropg  6072  rnpropg  6079  funprg  6408  funtp  6411  fntpg  6414  funcnvpr  6416  f1oprswap  6658  f1oprg  6659  fnimapr  6747  xpprsng  6902  residpr  6905  fpr  6916  fmptpr  6934  fvpr1  6952  fvpr1g  6954  fvpr2g  6955  df2o3  8117  enpr2d  8597  map2xp  8687  1sdom  8721  en2  8754  prfi  8793  prwf  9240  rankprb  9280  pr2nelem  9430  xp2dju  9602  ssxr  10710  prunioo  12868  prinfzo0  13077  fzosplitpr  13147  hashprg  13757  hashprlei  13827  s2prop  14269  s4prop  14272  f1oun2prg  14279  sumpr  15103  strle2  16593  phlstr  16653  symg2bas  18521  gsumpr  19075  dmdprdpr  19171  dprdpr  19172  lsmpr  19861  lsppr  19865  lspsntri  19869  lsppratlem1  19919  lsppratlem3  19921  lsppratlem4  19922  m2detleib  21240  xpstopnlem1  22417  ovolioo  24169  uniiccdif  24179  i1f1  24291  wilthlem2  25646  perfectlem2  25806  axlowdimlem13  26740  ex-dif  28202  ex-un  28203  ex-in  28204  ex-xp  28215  ex-cnv  28216  ex-rn  28219  ex-res  28220  spanpr  29357  superpos  30131  cnvprop  30432  brprop  30433  mptprop  30434  coprprop  30435  prct  30450  prodpr  30542  ccfldextdgrr  31057  esumpr  31325  eulerpartgbij  31630  signswch  31831  prodfzo03  31874  subfacp1lem1  32426  altopthsn  33422  onint1  33797  poimirlem8  34915  poimirlem9  34916  poimirlem15  34922  smprngopr  35345  dihprrnlem1N  38575  dihprrnlem2  38576  djhlsmat  38578  lclkrlem2c  38660  lclkrlem2v  38679  lcfrlem18  38711  pr2dom  39942  dfrcl4  40070  iunrelexp0  40096  corclrcl  40101  corcltrcl  40133  cotrclrcl  40136  mnuprdlem2  40658  sumpair  41341  rnfdmpr  43529  perfectALTVlem2  43936