Definition df-pr 4587

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

This definition is referenced by:  dfsn2  4597  dfpr2  4605  ralprgf  4655  rexprgf  4656  ralprg  4657  csbprg  4670  disjpr2  4674  prcom  4693  preq1  4694  qdass  4714  qdassr  4715  tpidm12  4716  prprc1  4726  difprsn1  4762  difpr  4765  tpprceq3  4766  snsspr1  4774  snsspr2  4775  prssg  4779  ssunpr  4794  sstp  4796  iunxprg  5055  iunopeqop  5492  iunopeqopOLD  5493  pwssun  5541  xpsspw  5784  dmpropg  6204  rnpropg  6211  funprg  6577  funtp  6580  fntpg  6583  funcnvpr  6585  f1oprswap  6854  f1oprg  6855  fnimapr  6952  xpprsng  7124  residpr  7127  fpr  7139  fmptpr  7158  fvpr1g  7176  f1ofvswap  7292  df2o3  8447  map2xp  9121  en2  9226  prfiALT  9271  prwf  9771  rankprb  9811  xp2dju  10135  ssxr  11254  prunioo  13487  prinfzo0  13706  fzosplitpr  13785  hashprg  14410  hashprlei  14483  s2prop  14922  s4prop  14925  f1oun2prg  14932  s2rn  14978  sumpr  15777  strle2  17197  phlstr  17377  symg2bas  19435  gsumpr  19997  dmdprdpr  20093  dprdpr  20094  lsmpr  21158  lsppr  21162  lspsntri  21166  lsppratlem1  21219  lsppratlem3  21221  lsppratlem4  21222  m2detleib  22693  xpstopnlem1  23871  ovolioo  25632  uniiccdif  25642  i1f1  25754  wilthlem2  27135  perfectlem2  27296  bdaypw2n0bndlem  28558  axlowdimlem13  29157  ex-dif  30627  ex-un  30628  ex-in  30629  ex-xp  30640  ex-cnv  30641  ex-rn  30644  ex-res  30645  spanpr  31785  superpos  32559  cnvprop  32900  brprop  32901  mptprop  32902  coprprop  32903  prct  32917  prodpr  33030  ccfldextdgrr  33971  esumpr  34365  eulerpartgbij  34671  signswch  34857  prodfzo03  34899  subfacp1lem1  35534  altopthsn  36316  onint1  36814  bj-prexg  37529  bj-prex  37530  bj-prfromadj  37535  poimirlem8  38132  poimirlem9  38133  poimirlem15  38139  smprngopr  38556  dihprrnlem1N  42053  dihprrnlem2  42054  djhlsmat  42056  lclkrlem2c  42138  lclkrlem2v  42157  lcfrlem18  42189  pr2dom  44108  dfrcl4  44257  iunrelexp0  44283  corclrcl  44288  corcltrcl  44320  cotrclrcl  44323  mnuprdlem2  44854  sumpair  45620  rnfdmpr  47880  perfectALTVlem2  48349  usgrexmpl2edg  48656