Definition df-pr 4580

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

This definition is referenced by:  dfsn2  4590  dfpr2  4598  ralprgf  4646  rexprgf  4647  ralprg  4648  csbprg  4661  disjpr2  4665  prcom  4684  preq1  4685  qdass  4705  qdassr  4706  tpidm12  4707  prprc1  4717  difprsn1  4751  difpr  4754  tpprceq3  4755  snsspr1  4765  snsspr2  4766  prssg  4770  ssunpr  4785  sstp  4787  iunxprg  5045  iunopeqop  5464  pwssun  5511  xpsspw  5752  dmpropg  6164  rnpropg  6171  funprg  6536  funtp  6539  fntpg  6542  funcnvpr  6544  f1oprswap  6808  f1oprg  6809  fnimapr  6906  xpprsng  7074  residpr  7077  fpr  7088  fmptpr  7108  fvpr1g  7126  f1ofvswap  7243  df2o3  8396  map2xp  9064  en2  9169  prfiALT  9214  prwf  9707  rankprb  9747  xp2dju  10071  ssxr  11185  prunioo  13384  prinfzo0  13601  fzosplitpr  13679  hashprg  14302  hashprlei  14375  s2prop  14814  s4prop  14817  f1oun2prg  14824  s2rn  14870  sumpr  15655  strle2  17070  phlstr  17250  symg2bas  19272  gsumpr  19834  dmdprdpr  19930  dprdpr  19931  lsmpr  20993  lsppr  20997  lspsntri  21001  lsppratlem1  21054  lsppratlem3  21056  lsppratlem4  21057  m2detleib  22516  xpstopnlem1  23694  ovolioo  25467  uniiccdif  25477  i1f1  25589  wilthlem2  26977  perfectlem2  27139  axlowdimlem13  28899  ex-dif  30367  ex-un  30368  ex-in  30369  ex-xp  30380  ex-cnv  30381  ex-rn  30384  ex-res  30385  spanpr  31524  superpos  32298  cnvprop  32639  brprop  32640  mptprop  32641  coprprop  32642  prct  32658  prodpr  32772  ccfldextdgrr  33645  esumpr  34039  eulerpartgbij  34346  signswch  34535  prodfzo03  34577  subfacp1lem1  35162  altopthsn  35945  onint1  36433  bj-prexg  37023  bj-prex  37024  bj-prfromadj  37029  poimirlem8  37618  poimirlem9  37619  poimirlem15  37625  smprngopr  38042  dihprrnlem1N  41413  dihprrnlem2  41414  djhlsmat  41416  lclkrlem2c  41498  lclkrlem2v  41517  lcfrlem18  41549  pr2dom  43510  dfrcl4  43659  iunrelexp0  43685  corclrcl  43690  corcltrcl  43722  cotrclrcl  43725  mnuprdlem2  44256  sumpair  45023  rnfdmpr  47275  perfectALTVlem2  47716  usgrexmpl2edg  48023