Definition df-pr 4651

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

This definition is referenced by:  dfsn2  4661  dfpr2  4668  ralprgf  4717  rexprgf  4718  ralprg  4719  csbprg  4734  disjpr2  4738  prcom  4757  preq1  4758  qdass  4778  qdassr  4779  tpidm12  4780  prprc1  4790  difprsn1  4825  difpr  4828  tpprceq3  4829  snsspr1  4839  snsspr2  4840  prssg  4844  ssunpr  4859  sstp  4861  iunxprg  5119  iunopeqop  5540  pwssun  5590  xpsspw  5828  dmpropg  6241  rnpropg  6248  funprg  6627  funtp  6630  fntpg  6633  funcnvpr  6635  f1oprswap  6901  f1oprg  6902  fnimapr  7000  xpprsng  7169  residpr  7172  fpr  7183  fmptpr  7201  fvpr1g  7219  fvpr2gOLD  7221  fvpr1OLD  7223  f1ofvswap  7337  df2o3  8524  enpr2dOLD  9110  map2xp  9207  1sdomOLD  9306  en2  9337  prfiALT  9386  prwf  9874  rankprb  9914  pr2nelemOLD  10066  xp2dju  10240  ssxr  11353  prunioo  13535  prinfzo0  13749  fzosplitpr  13820  hashprg  14438  hashprlei  14511  s2prop  14950  s4prop  14953  f1oun2prg  14960  s2rn  15006  sumpr  15790  strle2  17200  phlstr  17399  symg2bas  19428  gsumpr  19991  dmdprdpr  20087  dprdpr  20088  lsmpr  21105  lsppr  21109  lspsntri  21113  lsppratlem1  21166  lsppratlem3  21168  lsppratlem4  21169  m2detleib  22650  xpstopnlem1  23830  ovolioo  25614  uniiccdif  25624  i1f1  25736  wilthlem2  27122  perfectlem2  27284  axlowdimlem13  28979  ex-dif  30447  ex-un  30448  ex-in  30449  ex-xp  30460  ex-cnv  30461  ex-rn  30464  ex-res  30465  spanpr  31604  superpos  32378  cnvprop  32700  brprop  32701  mptprop  32702  coprprop  32703  prct  32720  prodpr  32822  ccfldextdgrr  33674  esumpr  34022  eulerpartgbij  34329  signswch  34530  prodfzo03  34572  subfacp1lem1  35139  altopthsn  35917  onint1  36407  bj-prexg  36997  bj-prex  36998  bj-prfromadj  37003  poimirlem8  37580  poimirlem9  37581  poimirlem15  37587  smprngopr  38004  dihprrnlem1N  41373  dihprrnlem2  41374  djhlsmat  41376  lclkrlem2c  41458  lclkrlem2v  41477  lcfrlem18  41509  pr2dom  43484  dfrcl4  43633  iunrelexp0  43659  corclrcl  43664  corcltrcl  43696  cotrclrcl  43699  mnuprdlem2  44237  sumpair  44924  rnfdmpr  47185  perfectALTVlem2  47585  usgrexmpl2edg  47833