Definition df-pr 3591

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

This definition is referenced by:  dfsn2  3598  dfpr2  3603  ralprg  3635  rexprg  3636  disjpr2  3648  prcom  3660  preq1  3661  qdass  3681  qdassr  3682  tpidm12  3683  prprc1  3692  difprsn1  3720  diftpsn3  3722  difpr  3723  snsspr1  3729  snsspr2  3730  prss  3737  prssg  3738  iunxprg  3954  2ordpr  4509  xpsspw  4724  dmpropg  5085  rnpropg  5092  funprg  5250  funtp  5253  fntpg  5256  f1oprg  5489  fnimapr  5560  fpr  5682  fprg  5683  fmptpr  5692  fvpr1  5704  fvpr1g  5706  fvpr2g  5707  df2o3  6413  enpr2d  6799  unfiexmid  6899  prfidisj  6908  pr2nelem  7172  xp2dju  7196  fzosplitprm1  10194  hashprg  10747  sumpr  11380  strle2g  12513  bdcpr  14023