Definition df-pr 3640

Description: Define unordered pair of classes. Definition 7.1 of [Quine] p. 48. They are unordered, so {𝐴, 𝐵} = {𝐵, 𝐴} as proven by prcom 3709. For a more traditional definition, but requiring a dummy variable, see dfpr2 3652. (Contributed by NM, 5-Aug-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 3634	. 2 class {𝐴, 𝐵}
4	1	csn 3633	. . 3 class {𝐴}
5	2	csn 3633	. . 3 class {𝐵}
6	4, 5	cun 3164	. 2 class ({𝐴} ∪ {𝐵})
7	3, 6	wceq 1373	1 wff {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})

This definition is referenced by:  dfsn2  3647  dfpr2  3652  ralprg  3684  rexprg  3685  disjpr2  3697  prcom  3709  preq1  3710  qdass  3730  qdassr  3731  tpidm12  3732  prprc1  3741  difprsn1  3772  diftpsn3  3774  difpr  3775  snsspr1  3781  snsspr2  3782  prss  3789  prssg  3790  iunxprg  4008  2ordpr  4572  xpsspw  4787  dmpropg  5155  rnpropg  5162  funprg  5324  funtp  5327  fntpg  5330  f1oprg  5566  fnimapr  5639  fpr  5766  fprg  5767  fmptpr  5776  fvpr1  5788  fvpr1g  5790  fvpr2g  5791  df2o3  6516  enpr2d  6911  unfiexmid  7015  prfidisj  7024  tpfidceq  7027  pr2nelem  7299  xp2dju  7327  fzosplitprm1  10363  hashprg  10953  sumpr  11724  strle2g  12939  perfectlem2  15472  bdcpr  15807