Definition df-pr 4627

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

This definition is referenced by:  dfsn2  4637  dfpr2  4644  ralprgf  4692  rexprgf  4693  ralprg  4694  csbprg  4707  disjpr2  4711  prcom  4730  preq1  4731  qdass  4751  qdassr  4752  tpidm12  4753  prprc1  4763  difprsn1  4798  difpr  4801  tpprceq3  4802  snsspr1  4812  snsspr2  4813  prssg  4817  ssunpr  4832  sstp  4834  iunxprg  5094  iunopeqop  5524  pwssun  5573  xpsspw  5817  dmpropg  6233  rnpropg  6240  funprg  6618  funtp  6621  fntpg  6624  funcnvpr  6626  f1oprswap  6890  f1oprg  6891  fnimapr  6990  xpprsng  7158  residpr  7161  fpr  7172  fmptpr  7190  fvpr1g  7208  f1ofvswap  7324  df2o3  8510  enpr2dOLD  9086  map2xp  9183  1sdomOLD  9281  en2  9311  prfiALT  9360  prwf  9847  rankprb  9887  pr2nelemOLD  10039  xp2dju  10213  ssxr  11326  prunioo  13517  prinfzo0  13734  fzosplitpr  13811  hashprg  14430  hashprlei  14503  s2prop  14942  s4prop  14945  f1oun2prg  14952  s2rn  14998  sumpr  15780  strle2  17192  phlstr  17386  symg2bas  19406  gsumpr  19969  dmdprdpr  20065  dprdpr  20066  lsmpr  21080  lsppr  21084  lspsntri  21088  lsppratlem1  21141  lsppratlem3  21143  lsppratlem4  21144  m2detleib  22627  xpstopnlem1  23807  ovolioo  25593  uniiccdif  25603  i1f1  25715  wilthlem2  27102  perfectlem2  27264  axlowdimlem13  28959  ex-dif  30432  ex-un  30433  ex-in  30434  ex-xp  30445  ex-cnv  30446  ex-rn  30449  ex-res  30450  spanpr  31589  superpos  32363  cnvprop  32694  brprop  32695  mptprop  32696  coprprop  32697  prct  32715  prodpr  32816  ccfldextdgrr  33707  esumpr  34045  eulerpartgbij  34352  signswch  34554  prodfzo03  34596  subfacp1lem1  35162  altopthsn  35940  onint1  36428  bj-prexg  37018  bj-prex  37019  bj-prfromadj  37024  poimirlem8  37613  poimirlem9  37614  poimirlem15  37620  smprngopr  38037  dihprrnlem1N  41404  dihprrnlem2  41405  djhlsmat  41407  lclkrlem2c  41489  lclkrlem2v  41508  lcfrlem18  41540  pr2dom  43518  dfrcl4  43667  iunrelexp0  43693  corclrcl  43698  corcltrcl  43730  cotrclrcl  43733  mnuprdlem2  44270  sumpair  45016  rnfdmpr  47269  perfectALTVlem2  47685  usgrexmpl2edg  47964