Definition df-pr 4571

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

This definition is referenced by:  dfsn2  4581  dfpr2  4589  ralprgf  4639  rexprgf  4640  ralprg  4641  csbprg  4654  disjpr2  4658  prcom  4677  preq1  4678  qdass  4698  qdassr  4699  tpidm12  4700  prprc1  4710  difprsn1  4746  difpr  4749  tpprceq3  4750  snsspr1  4758  snsspr2  4759  prssg  4763  ssunpr  4778  sstp  4780  iunxprg  5039  iunopeqop  5473  pwssun  5520  xpsspw  5762  dmpropg  6177  rnpropg  6184  funprg  6550  funtp  6553  fntpg  6556  funcnvpr  6558  f1oprswap  6823  f1oprg  6824  fnimapr  6921  xpprsng  7091  residpr  7094  fpr  7105  fmptpr  7124  fvpr1g  7142  f1ofvswap  7258  df2o3  8410  map2xp  9082  en2  9187  prfiALT  9232  prwf  9732  rankprb  9772  xp2dju  10096  ssxr  11212  prunioo  13431  prinfzo0  13650  fzosplitpr  13729  hashprg  14354  hashprlei  14427  s2prop  14866  s4prop  14869  f1oun2prg  14876  s2rn  14922  sumpr  15707  strle2  17126  phlstr  17306  symg2bas  19365  gsumpr  19927  dmdprdpr  20023  dprdpr  20024  lsmpr  21081  lsppr  21085  lspsntri  21089  lsppratlem1  21142  lsppratlem3  21144  lsppratlem4  21145  m2detleib  22593  xpstopnlem1  23771  ovolioo  25532  uniiccdif  25542  i1f1  25654  wilthlem2  27029  perfectlem2  27190  bdaypw2n0bndlem  28452  axlowdimlem13  29020  ex-dif  30490  ex-un  30491  ex-in  30492  ex-xp  30503  ex-cnv  30504  ex-rn  30507  ex-res  30508  spanpr  31648  superpos  32422  cnvprop  32766  brprop  32767  mptprop  32768  coprprop  32769  prct  32783  prodpr  32896  ccfldextdgrr  33813  esumpr  34207  eulerpartgbij  34513  signswch  34702  prodfzo03  34744  subfacp1lem1  35358  altopthsn  36140  onint1  36628  bj-prexg  37343  bj-prex  37344  bj-prfromadj  37349  poimirlem8  37946  poimirlem9  37947  poimirlem15  37953  smprngopr  38370  dihprrnlem1N  41867  dihprrnlem2  41868  djhlsmat  41870  lclkrlem2c  41952  lclkrlem2v  41971  lcfrlem18  42003  pr2dom  43951  dfrcl4  44100  iunrelexp0  44126  corclrcl  44131  corcltrcl  44163  cotrclrcl  44166  mnuprdlem2  44697  sumpair  45463  rnfdmpr  47720  perfectALTVlem2  48189  usgrexmpl2edg  48496