Definition df-pr 4585

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

This definition is referenced by:  dfsn2  4595  dfpr2  4603  ralprgf  4653  rexprgf  4654  ralprg  4655  csbprg  4668  disjpr2  4672  prcom  4691  preq1  4692  qdass  4712  qdassr  4713  tpidm12  4714  prprc1  4724  difprsn1  4758  difpr  4761  tpprceq3  4762  snsspr1  4772  snsspr2  4773  prssg  4777  ssunpr  4792  sstp  4794  iunxprg  5053  iunopeqop  5479  pwssun  5526  xpsspw  5768  dmpropg  6183  rnpropg  6190  funprg  6556  funtp  6559  fntpg  6562  funcnvpr  6564  f1oprswap  6829  f1oprg  6830  fnimapr  6927  xpprsng  7097  residpr  7100  fpr  7111  fmptpr  7130  fvpr1g  7148  f1ofvswap  7264  df2o3  8417  map2xp  9089  en2  9194  prfiALT  9239  prwf  9737  rankprb  9777  xp2dju  10101  ssxr  11216  prunioo  13411  prinfzo0  13628  fzosplitpr  13707  hashprg  14332  hashprlei  14405  s2prop  14844  s4prop  14847  f1oun2prg  14854  s2rn  14900  sumpr  15685  strle2  17100  phlstr  17280  symg2bas  19339  gsumpr  19901  dmdprdpr  19997  dprdpr  19998  lsmpr  21058  lsppr  21062  lspsntri  21066  lsppratlem1  21119  lsppratlem3  21121  lsppratlem4  21122  m2detleib  22592  xpstopnlem1  23770  ovolioo  25542  uniiccdif  25552  i1f1  25664  wilthlem2  27052  perfectlem2  27214  bdaypw2n0bndlem  28476  axlowdimlem13  29045  ex-dif  30516  ex-un  30517  ex-in  30518  ex-xp  30529  ex-cnv  30530  ex-rn  30533  ex-res  30534  spanpr  31674  superpos  32448  cnvprop  32792  brprop  32793  mptprop  32794  coprprop  32795  prct  32809  prodpr  32924  ccfldextdgrr  33856  esumpr  34250  eulerpartgbij  34556  signswch  34745  prodfzo03  34787  subfacp1lem1  35401  altopthsn  36183  onint1  36671  bj-prexg  37314  bj-prex  37315  bj-prfromadj  37320  poimirlem8  37908  poimirlem9  37909  poimirlem15  37915  smprngopr  38332  dihprrnlem1N  41829  dihprrnlem2  41830  djhlsmat  41832  lclkrlem2c  41914  lclkrlem2v  41933  lcfrlem18  41965  pr2dom  43912  dfrcl4  44061  iunrelexp0  44087  corclrcl  44092  corcltrcl  44124  cotrclrcl  44127  mnuprdlem2  44658  sumpair  45424  rnfdmpr  47670  perfectALTVlem2  48111  usgrexmpl2edg  48418