Definition df-pr 4530

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

This definition is referenced by:  dfsn2  4540  dfpr2  4546  ralprgf  4594  rexprgf  4595  ralprg  4596  csbprg  4611  disjpr2  4615  prcom  4634  preq1  4635  qdass  4655  qdassr  4656  tpidm12  4657  prprc1  4667  difprsn1  4699  difpr  4702  tpprceq3  4703  snsspr1  4713  snsspr2  4714  prssg  4718  ssunpr  4731  sstp  4733  iunxprg  4990  iunopeqop  5389  pwssun  5436  xpsspw  5664  dmpropg  6058  rnpropg  6065  funprg  6412  funtp  6415  fntpg  6418  funcnvpr  6420  f1oprswap  6682  f1oprg  6683  fnimapr  6773  xpprsng  6933  residpr  6936  fpr  6947  fmptpr  6965  fvpr1  6983  fvpr1g  6985  fvpr2g  6986  f1ofvswap  7094  df2o3  8195  enpr2d  8703  map2xp  8794  1sdom  8857  en2  8888  prfi  8924  prwf  9392  rankprb  9432  pr2nelem  9583  xp2dju  9755  ssxr  10867  prunioo  13034  prinfzo0  13246  fzosplitpr  13316  hashprg  13927  hashprlei  13999  s2prop  14437  s4prop  14440  f1oun2prg  14447  sumpr  15275  strle2  16777  phlstr  16837  symg2bas  18739  gsumpr  19294  dmdprdpr  19390  dprdpr  19391  lsmpr  20080  lsppr  20084  lspsntri  20088  lsppratlem1  20138  lsppratlem3  20140  lsppratlem4  20141  m2detleib  21482  xpstopnlem1  22660  ovolioo  24419  uniiccdif  24429  i1f1  24541  wilthlem2  25905  perfectlem2  26065  axlowdimlem13  26999  ex-dif  28460  ex-un  28461  ex-in  28462  ex-xp  28473  ex-cnv  28474  ex-rn  28477  ex-res  28478  spanpr  29615  superpos  30389  cnvprop  30703  brprop  30704  mptprop  30705  coprprop  30706  prct  30723  prodpr  30814  ccfldextdgrr  31410  esumpr  31700  eulerpartgbij  32005  signswch  32206  prodfzo03  32249  subfacp1lem1  32808  altopthsn  33949  onint1  34324  poimirlem8  35471  poimirlem9  35472  poimirlem15  35478  smprngopr  35896  dihprrnlem1N  39124  dihprrnlem2  39125  djhlsmat  39127  lclkrlem2c  39209  lclkrlem2v  39228  lcfrlem18  39260  pr2dom  40760  dfrcl4  40902  iunrelexp0  40928  corclrcl  40933  corcltrcl  40965  cotrclrcl  40968  mnuprdlem2  41505  sumpair  42192  rnfdmpr  44388  perfectALTVlem2  44790