Definition df-pr 3382

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

This definition is referenced by:  dfsn2  3389  dfpr2  3394  ralprg  3421  rexprg  3422  disjpr2  3434  prcom  3446  preq1  3447  qdass  3467  qdassr  3468  tpidm12  3469  prprc1  3478  difprsn1  3503  diftpsn3  3505  snsspr1  3512  snsspr2  3513  prss  3520  prssg  3521  2ordpr  4249  xpsspw  4450  dmpropg  4793  rnpropg  4800  funprg  4949  funtp  4952  fntpg  4955  f1oprg  5168  fnimapr  5233  fpr  5345  fprg  5346  fmptpr  5355  fvpr1  5365  fvpr1g  5367  fvpr2g  5368  df2o3  6014  fzosplitprm1  9090  bdcpr  9991