Definition df-pr 3498

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

This definition is referenced by:  dfsn2  3505  dfpr2  3510  ralprg  3538  rexprg  3539  disjpr2  3551  prcom  3563  preq1  3564  qdass  3584  qdassr  3585  tpidm12  3586  prprc1  3595  difprsn1  3623  diftpsn3  3625  difpr  3626  snsspr1  3632  snsspr2  3633  prss  3640  prssg  3641  iunxprg  3857  2ordpr  4397  xpsspw  4609  dmpropg  4967  rnpropg  4974  funprg  5129  funtp  5132  fntpg  5135  f1oprg  5363  fnimapr  5433  fpr  5554  fprg  5555  fmptpr  5564  fvpr1  5576  fvpr1g  5578  fvpr2g  5579  df2o3  6279  unfiexmid  6757  prfidisj  6766  pr2nelem  6994  xp2dju  7016  fzosplitprm1  9898  hashprg  10441  sumpr  11068  strle2g  11887  bdcpr  12752