Definition df-pr 4631

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

This definition is referenced by:  dfsn2  4641  dfpr2  4647  ralprgf  4696  rexprgf  4697  ralprg  4698  csbprg  4713  disjpr2  4717  prcom  4736  preq1  4737  qdass  4757  qdassr  4758  tpidm12  4759  prprc1  4769  difprsn1  4803  difpr  4806  tpprceq3  4807  snsspr1  4817  snsspr2  4818  prssg  4822  ssunpr  4835  sstp  4837  iunxprg  5099  iunopeqop  5521  pwssun  5571  xpsspw  5808  dmpropg  6212  rnpropg  6219  funprg  6600  funtp  6603  fntpg  6606  funcnvpr  6608  f1oprswap  6875  f1oprg  6876  fnimapr  6973  xpprsng  7135  residpr  7138  fpr  7149  fmptpr  7167  fvpr1g  7185  fvpr2gOLD  7187  fvpr1OLD  7189  f1ofvswap  7301  df2o3  8471  enpr2dOLD  9047  map2xp  9144  1sdomOLD  9246  en2  9278  prfi  9319  prwf  9803  rankprb  9843  pr2nelemOLD  9995  xp2dju  10168  ssxr  11280  prunioo  13455  prinfzo0  13668  fzosplitpr  13738  hashprg  14352  hashprlei  14426  s2prop  14855  s4prop  14858  f1oun2prg  14865  sumpr  15691  strle2  17089  phlstr  17288  symg2bas  19255  gsumpr  19818  dmdprdpr  19914  dprdpr  19915  lsmpr  20693  lsppr  20697  lspsntri  20701  lsppratlem1  20753  lsppratlem3  20755  lsppratlem4  20756  m2detleib  22125  xpstopnlem1  23305  ovolioo  25077  uniiccdif  25087  i1f1  25199  wilthlem2  26563  perfectlem2  26723  axlowdimlem13  28202  ex-dif  29666  ex-un  29667  ex-in  29668  ex-xp  29679  ex-cnv  29680  ex-rn  29683  ex-res  29684  spanpr  30821  superpos  31595  cnvprop  31906  brprop  31907  mptprop  31908  coprprop  31909  prct  31927  prodpr  32020  ccfldextdgrr  32735  esumpr  33053  eulerpartgbij  33360  signswch  33561  prodfzo03  33604  subfacp1lem1  34159  altopthsn  34922  onint1  35323  bj-prexg  35909  bj-prex  35910  bj-prfromadj  35915  poimirlem8  36485  poimirlem9  36486  poimirlem15  36492  smprngopr  36909  dihprrnlem1N  40284  dihprrnlem2  40285  djhlsmat  40287  lclkrlem2c  40369  lclkrlem2v  40388  lcfrlem18  40420  pr2dom  42264  dfrcl4  42413  iunrelexp0  42439  corclrcl  42444  corcltrcl  42476  cotrclrcl  42479  mnuprdlem2  43018  sumpair  43705  rnfdmpr  45976  perfectALTVlem2  46377