Definition df-pr 3600

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

This definition is referenced by:  dfsn2  3607  dfpr2  3612  ralprg  3644  rexprg  3645  disjpr2  3657  prcom  3669  preq1  3670  qdass  3690  qdassr  3691  tpidm12  3692  prprc1  3701  difprsn1  3732  diftpsn3  3734  difpr  3735  snsspr1  3741  snsspr2  3742  prss  3749  prssg  3750  iunxprg  3968  2ordpr  4524  xpsspw  4739  dmpropg  5102  rnpropg  5109  funprg  5267  funtp  5270  fntpg  5273  f1oprg  5506  fnimapr  5577  fpr  5699  fprg  5700  fmptpr  5709  fvpr1  5721  fvpr1g  5723  fvpr2g  5724  df2o3  6431  enpr2d  6817  unfiexmid  6917  prfidisj  6926  pr2nelem  7190  xp2dju  7214  fzosplitprm1  10234  hashprg  10788  sumpr  11421  strle2g  12566  bdcpr  14626