Definition df-pr 4586

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

This definition is used by:  dfsn2  4596  dfpr2  4604  ralprgf  4654  rexprgf  4655  ralprg  4656  csbprg  4669  disjpr2  4673  prcom  4692  preq1  4693  qdass  4713  qdassr  4714  tpidm12  4715  prprc1  4725  difprsn1  4762  difpr  4765  tpprceq3  4766  snsspr1  4774  snsspr2  4775  prssg  4779  ssunpr  4793  sstp  4795  iunxprg  5055  iunopeqop  5493  iunopeqopOLD  5494  pwssun  5542  xpsspw  5786  dmpropg  6216  rnpropg  6223  funprg  6594  funtp  6597  fntpg  6600  funcnvpr  6602  f1oprswap  6870  f1oprg  6871  fnimapr  6968  xpprsng  7142  xpsnprg  7143  xpsntpg  7144  residpr  7146  fpr  7158  fmptpr  7177  fvpr1g  7195  f1ofvswap  7314  df2o3  8484  map2xp  9166  en2  9271  prfiALT  9316  prwf  9819  rankprb  9865  xp2dju  10255  ssxr  11379  prunioo  13612  prinfzo0  13833  fzosplitpr  13912  hashprg  14539  hashprlei  14613  s2prop  15058  s4prop  15061  f1oun2prg  15068  s2rn  15116  sumpr  15914  strle2  17337  phlstr  17517  symg2bas  19607  gsumpr  20169  dmdprdpr  20265  dprdpr  20266  lsmpr  21364  lsppr  21368  lspsntri  21372  lsppratlem1  21425  lsppratlem3  21427  lsppratlem4  21428  m2detleib  22946  xpstopnlem1  24128  ovolioo  25889  uniiccdif  25899  i1f1  26011  wilthlem2  27396  perfectlem2  27557  bdaypw2n0bndlem  28849  axlowdimlem13  29532  ex-dif  31024  ex-un  31025  ex-in  31026  ex-xp  31037  ex-cnv  31038  ex-rn  31041  ex-res  31042  spanpr  32182  superpos  32956  cnvprop  33331  brprop  33332  mptprop  33333  coprprop  33334  prct  33348  prodpr  33459  ccfldextdgrr  34346  esumpr  34740  eulerpartgbij  35046  signswch  35232  prodfzo03  35274  subfacp1lem1  35986  altopthsn  36768  onint1  37279  bj-prexg  37994  bj-prex  37995  bj-prfromadj  38000  poimirlem8  38589  poimirlem9  38590  poimirlem15  38596  smprngopr  39029  dihprrnlem1N  42524  dihprrnlem2  42525  djhlsmat  42527  lclkrlem2c  42609  lclkrlem2v  42628  lcfrlem18  42660  pr2dom  44570  dfrcl4  44718  iunrelexp0  44744  corclrcl  44749  corcltrcl  44781  cotrclrcl  44784  mnuprdlem2  45299  hfpr  46058  sumpair  46094  rnfdmpr  48393  perfectALTVlem2  48862  usgrexmpl2edg  49169  smprngprmrng  49478