Definition df-pr 3438

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

This definition is referenced by:  dfsn2  3445  dfpr2  3450  ralprg  3478  rexprg  3479  disjpr2  3491  prcom  3503  preq1  3504  qdass  3524  qdassr  3525  tpidm12  3526  prprc1  3535  difprsn1  3561  diftpsn3  3563  difpr  3564  snsspr1  3570  snsspr2  3571  prss  3578  prssg  3579  2ordpr  4315  xpsspw  4520  dmpropg  4871  rnpropg  4878  funprg  5031  funtp  5034  fntpg  5037  f1oprg  5260  fnimapr  5329  fpr  5444  fprg  5445  fmptpr  5454  fvpr1  5464  fvpr1g  5466  fvpr2g  5467  df2o3  6151  unfiexmid  6582  prfidisj  6591  pr2nelem  6766  fzosplitprm1  9576  hashprg  10116  sumpr  10694  bdcpr  11231