Definition df-pr 4633

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

This definition is referenced by:  dfsn2  4643  dfpr2  4650  ralprgf  4698  rexprgf  4699  ralprg  4700  csbprg  4713  disjpr2  4717  prcom  4736  preq1  4737  qdass  4757  qdassr  4758  tpidm12  4759  prprc1  4769  difprsn1  4804  difpr  4807  tpprceq3  4808  snsspr1  4818  snsspr2  4819  prssg  4823  ssunpr  4838  sstp  4840  iunxprg  5099  iunopeqop  5520  pwssun  5569  xpsspw  5811  dmpropg  6226  rnpropg  6233  funprg  6611  funtp  6614  fntpg  6617  funcnvpr  6619  f1oprswap  6881  f1oprg  6882  fnimapr  6980  xpprsng  7148  residpr  7151  fpr  7162  fmptpr  7180  fvpr1g  7198  f1ofvswap  7314  df2o3  8500  enpr2dOLD  9076  map2xp  9173  1sdomOLD  9270  en2  9300  prfiALT  9349  prwf  9835  rankprb  9875  pr2nelemOLD  10027  xp2dju  10201  ssxr  11314  prunioo  13504  prinfzo0  13721  fzosplitpr  13798  hashprg  14417  hashprlei  14490  s2prop  14929  s4prop  14932  f1oun2prg  14939  s2rn  14985  sumpr  15767  strle2  17179  phlstr  17378  symg2bas  19408  gsumpr  19971  dmdprdpr  20067  dprdpr  20068  lsmpr  21085  lsppr  21089  lspsntri  21093  lsppratlem1  21146  lsppratlem3  21148  lsppratlem4  21149  m2detleib  22632  xpstopnlem1  23812  ovolioo  25596  uniiccdif  25606  i1f1  25718  wilthlem2  27106  perfectlem2  27268  axlowdimlem13  28963  ex-dif  30431  ex-un  30432  ex-in  30433  ex-xp  30444  ex-cnv  30445  ex-rn  30448  ex-res  30449  spanpr  31588  superpos  32362  cnvprop  32682  brprop  32683  mptprop  32684  coprprop  32685  prct  32702  prodpr  32803  ccfldextdgrr  33654  esumpr  34002  eulerpartgbij  34309  signswch  34510  prodfzo03  34552  subfacp1lem1  35119  altopthsn  35898  onint1  36387  bj-prexg  36977  bj-prex  36978  bj-prfromadj  36983  poimirlem8  37570  poimirlem9  37571  poimirlem15  37577  smprngopr  37994  dihprrnlem1N  41362  dihprrnlem2  41363  djhlsmat  41365  lclkrlem2c  41447  lclkrlem2v  41466  lcfrlem18  41498  pr2dom  43476  dfrcl4  43625  iunrelexp0  43651  corclrcl  43656  corcltrcl  43688  cotrclrcl  43691  mnuprdlem2  44229  sumpair  44933  rnfdmpr  47193  perfectALTVlem2  47609  usgrexmpl2edg  47886