Definition df-pr 4438

Description: Define unordered pair of classes. Definition 7.1 of [Quine] p. 48. For example, 𝐴 ∈ {1, -1} → (𝐴↑2) = 1 (ex-pr 28002). They are unordered, so {𝐴, 𝐵} = {𝐵, 𝐴} as proven by prcom 4538. For a more traditional definition, but requiring a dummy variable, see dfpr2 4454. {𝐴, 𝐴} is also an unordered pair, but also a singleton because of {𝐴} = {𝐴, 𝐴} (see dfsn2 4448). Therefore, {𝐴, 𝐵} is called a proper (unordered) pair iff 𝐴 ≠ 𝐵 and 𝐴 and 𝐵 are sets. (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 4437	. 2 class {𝐴, 𝐵}
4	1	csn 4435	. . 3 class {𝐴}
5	2	csn 4435	. . 3 class {𝐵}
6	4, 5	cun 3820	. 2 class ({𝐴} ∪ {𝐵})
7	3, 6	wceq 1508	1 wff {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})

This definition is referenced by:  dfsn2  4448  dfpr2  4454  ralprgf  4500  rexprgf  4501  csbprg  4515  disjpr2  4519  prcom  4538  preq1  4539  qdass  4559  qdassr  4560  tpidm12  4561  prprc1  4571  difprsn1  4603  difpr  4606  tpprceq3  4607  snsspr1  4617  snsspr2  4618  prssg  4622  ssunpr  4635  sstp  4637  iunxprg  4880  iunopeqop  5263  pwssun  5304  xpsspw  5528  dmpropg  5908  rnpropg  5915  funprg  6238  funtp  6241  fntpg  6244  funcnvpr  6246  f1oprswap  6484  f1oprg  6485  fnimapr  6573  xpprsng  6723  residpr  6726  fpr  6737  fmptpr  6755  fvpr1  6777  fvpr1g  6779  fvpr2g  6780  df2o3  7917  map2xp  8481  1sdom  8514  en2  8547  prfi  8586  prwf  9032  rankprb  9072  pr2nelem  9222  xp2dju  9398  ssxr  10508  prunioo  12681  prinfzo0  12889  fzosplitpr  12959  hashprg  13567  hashprlei  13635  s2prop  14129  s4prop  14132  f1oun2prg  14139  sumpr  14961  strle2  16447  phlstr  16507  xpscg  16685  symg2bas  18299  gsumpr  18840  dmdprdpr  18933  dprdpr  18934  lsmpr  19595  lsppr  19599  lspsntri  19603  lsppratlem1  19653  lsppratlem3  19655  lsppratlem4  19656  m2detleib  20959  xpstopnlem1  22136  ovolioo  23887  uniiccdif  23897  i1f1  24009  wilthlem2  25363  perfectlem2  25523  axlowdimlem13  26458  ex-dif  27995  ex-un  27996  ex-in  27997  ex-xp  28008  ex-cnv  28009  ex-rn  28012  ex-res  28013  spanpr  29153  superpos  29927  cnvprop  30208  brprop  30209  mptprop  30210  coprprop  30211  prct  30226  prodpr  30312  ccfldextdgrr  30718  esumpr  31001  eulerpartgbij  31307  signswch  31509  prodfzo03  31554  subfacp1lem1  32048  altopthsn  32980  onint1  33354  poimirlem8  34378  poimirlem9  34379  poimirlem15  34385  smprngopr  34809  dihprrnlem1N  38042  dihprrnlem2  38043  djhlsmat  38045  lclkrlem2c  38127  lclkrlem2v  38146  lcfrlem18  38178  dfrcl4  39422  iunrelexp0  39448  corclrcl  39453  corcltrcl  39485  cotrclrcl  39488  enpr2d  39967  mnuprdlem2  40022  sumpair  40749  rnfdmpr  42920  perfectALTVlem2  43289