Definition df-pr 4577

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

This definition is referenced by:  dfsn2  4587  dfpr2  4593  ralprgf  4641  rexprgf  4642  ralprg  4643  csbprg  4658  disjpr2  4662  prcom  4681  preq1  4682  qdass  4702  qdassr  4703  tpidm12  4704  prprc1  4714  difprsn1  4748  difpr  4751  tpprceq3  4752  snsspr1  4762  snsspr2  4763  prssg  4767  ssunpr  4780  sstp  4782  iunxprg  5044  iunopeqop  5466  pwssun  5516  xpsspw  5752  dmpropg  6154  rnpropg  6161  funprg  6539  funtp  6542  fntpg  6545  funcnvpr  6547  f1oprswap  6812  f1oprg  6813  fnimapr  6909  xpprsng  7069  residpr  7072  fpr  7083  fmptpr  7101  fvpr1g  7119  fvpr2gOLD  7121  fvpr1OLD  7123  f1ofvswap  7235  df2o3  8376  enpr2dOLD  8916  map2xp  9013  1sdomOLD  9115  en2  9147  prfi  9188  prwf  9669  rankprb  9709  pr2nelemOLD  9861  xp2dju  10034  ssxr  11146  prunioo  13315  prinfzo0  13528  fzosplitpr  13598  hashprg  14211  hashprlei  14283  s2prop  14720  s4prop  14723  f1oun2prg  14730  sumpr  15560  strle2  16958  phlstr  17154  symg2bas  19097  gsumpr  19652  dmdprdpr  19748  dprdpr  19749  lsmpr  20458  lsppr  20462  lspsntri  20466  lsppratlem1  20516  lsppratlem3  20518  lsppratlem4  20519  m2detleib  21887  xpstopnlem1  23067  ovolioo  24839  uniiccdif  24849  i1f1  24961  wilthlem2  26325  perfectlem2  26485  axlowdimlem13  27612  ex-dif  29076  ex-un  29077  ex-in  29078  ex-xp  29089  ex-cnv  29090  ex-rn  29093  ex-res  29094  spanpr  30231  superpos  31005  cnvprop  31316  brprop  31317  mptprop  31318  coprprop  31319  prct  31336  prodpr  31427  ccfldextdgrr  32040  esumpr  32332  eulerpartgbij  32639  signswch  32840  prodfzo03  32883  subfacp1lem1  33440  altopthsn  34402  onint1  34777  bj-prexg  35366  bj-prex  35367  bj-prfromadj  35372  poimirlem8  35941  poimirlem9  35942  poimirlem15  35948  smprngopr  36366  dihprrnlem1N  39743  dihprrnlem2  39744  djhlsmat  39746  lclkrlem2c  39828  lclkrlem2v  39847  lcfrlem18  39879  pr2dom  41508  dfrcl4  41657  iunrelexp0  41683  corclrcl  41688  corcltrcl  41720  cotrclrcl  41723  mnuprdlem2  42264  sumpair  42951  rnfdmpr  45191  perfectALTVlem2  45592