Definition df-pr 4581

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 4687. For a more traditional definition, but requiring a dummy variable, see dfpr2 4599. {𝐴, 𝐴} is also an unordered pair, but also a singleton because of {𝐴} = {𝐴, 𝐴} (see dfsn2 4591). 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 4585. 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 4580	. 2 class {𝐴, 𝐵}
4	1	csn 4578	. . 3 class {𝐴}
5	2	csn 4578	. . 3 class {𝐵}
6	4, 5	cun 3897	. 2 class ({𝐴} ∪ {𝐵})
7	3, 6	wceq 1541	1 wff {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})

This definition is referenced by:  dfsn2  4591  dfpr2  4599  ralprgf  4649  rexprgf  4650  ralprg  4651  csbprg  4664  disjpr2  4668  prcom  4687  preq1  4688  qdass  4708  qdassr  4709  tpidm12  4710  prprc1  4720  difprsn1  4754  difpr  4757  tpprceq3  4758  snsspr1  4768  snsspr2  4769  prssg  4773  ssunpr  4788  sstp  4790  iunxprg  5049  iunopeqop  5467  pwssun  5514  xpsspw  5756  dmpropg  6171  rnpropg  6178  funprg  6544  funtp  6547  fntpg  6550  funcnvpr  6552  f1oprswap  6817  f1oprg  6818  fnimapr  6915  xpprsng  7083  residpr  7086  fpr  7097  fmptpr  7116  fvpr1g  7134  f1ofvswap  7250  df2o3  8403  map2xp  9073  en2  9178  prfiALT  9223  prwf  9721  rankprb  9761  xp2dju  10085  ssxr  11200  prunioo  13395  prinfzo0  13612  fzosplitpr  13691  hashprg  14316  hashprlei  14389  s2prop  14828  s4prop  14831  f1oun2prg  14838  s2rn  14884  sumpr  15669  strle2  17084  phlstr  17264  symg2bas  19320  gsumpr  19882  dmdprdpr  19978  dprdpr  19979  lsmpr  21039  lsppr  21043  lspsntri  21047  lsppratlem1  21100  lsppratlem3  21102  lsppratlem4  21103  m2detleib  22573  xpstopnlem1  23751  ovolioo  25523  uniiccdif  25533  i1f1  25645  wilthlem2  27033  perfectlem2  27195  bdaypw2n0s  28420  axlowdimlem13  28976  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  32724  brprop  32725  mptprop  32726  coprprop  32727  prct  32741  prodpr  32856  ccfldextdgrr  33778  esumpr  34172  eulerpartgbij  34478  signswch  34667  prodfzo03  34709  subfacp1lem1  35322  altopthsn  36104  onint1  36592  bj-prexg  37183  bj-prex  37184  bj-prfromadj  37189  poimirlem8  37768  poimirlem9  37769  poimirlem15  37775  smprngopr  38192  dihprrnlem1N  41623  dihprrnlem2  41624  djhlsmat  41626  lclkrlem2c  41708  lclkrlem2v  41727  lcfrlem18  41759  pr2dom  43710  dfrcl4  43859  iunrelexp0  43885  corclrcl  43890  corcltrcl  43922  cotrclrcl  43925  mnuprdlem2  44456  sumpair  45222  rnfdmpr  47469  perfectALTVlem2  47910  usgrexmpl2edg  48217