Definition df-pr 3583

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

This definition is referenced by:  dfsn2  3590  dfpr2  3595  ralprg  3627  rexprg  3628  disjpr2  3640  prcom  3652  preq1  3653  qdass  3673  qdassr  3674  tpidm12  3675  prprc1  3684  difprsn1  3712  diftpsn3  3714  difpr  3715  snsspr1  3721  snsspr2  3722  prss  3729  prssg  3730  iunxprg  3946  2ordpr  4501  xpsspw  4716  dmpropg  5076  rnpropg  5083  funprg  5238  funtp  5241  fntpg  5244  f1oprg  5476  fnimapr  5546  fpr  5667  fprg  5668  fmptpr  5677  fvpr1  5689  fvpr1g  5691  fvpr2g  5692  df2o3  6398  enpr2d  6783  unfiexmid  6883  prfidisj  6892  pr2nelem  7147  xp2dju  7171  fzosplitprm1  10169  hashprg  10721  sumpr  11354  strle2g  12486  bdcpr  13753