Definition df-pr 3673

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

This definition is referenced by:  dfsn2  3680  dfpr2  3685  ralprg  3717  rexprg  3718  disjpr2  3730  prcom  3742  preq1  3743  qdass  3763  qdassr  3764  tpidm12  3765  prprc1  3775  difprsn1  3807  diftpsn3  3809  difpr  3810  snsspr1  3816  snsspr2  3817  prss  3824  prssg  3825  iunxprg  4046  2ordpr  4616  xpsspw  4831  dmpropg  5201  rnpropg  5208  funprg  5371  funtp  5374  fntpg  5377  f1oprg  5619  fnimapr  5696  fpr  5825  fprg  5826  fmptpr  5835  fvpr1  5847  fvpr1g  5849  fvpr2g  5850  df2o3  6583  enpr2d  6980  unfiexmid  7091  prfidisj  7100  tpfidceq  7103  pr2nelem  7375  xp2dju  7408  fzosplitprm1  10452  hashprg  11043  sumpr  11939  strle2g  13155  perfectlem2  15689  bdcpr  16289