Definition df-pr 3701

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

This definition is referenced by:  dfsn2  3708  dfpr2  3713  ralprg  3745  rexprg  3746  disjpr2  3758  prcom  3772  preq1  3773  qdass  3793  qdassr  3794  tpidm12  3795  prprc1  3805  difprsn1  3838  diftpsn3  3840  difpr  3841  snsspr1  3847  snsspr2  3848  prss  3855  prssg  3856  iunxprg  4077  2ordpr  4651  xpsspw  4867  dmpropg  5240  rnpropg  5247  funprg  5411  funtp  5414  fntpg  5417  f1oprg  5665  fnimapr  5742  fpr  5871  fprg  5872  fmptpr  5881  fvpr1  5893  fvpr1g  5895  fvpr2g  5896  df2o3  6675  enpr2d  7077  unfiexmid  7191  prfidisj  7200  tpfidceq  7203  pr2nelem  7501  xp2dju  7535  fzosplitpr  10601  fzosplitprm1  10602  hashprg  11198  sumpr  12124  strle2g  13404  perfectlem2  15994  bdcpr  16767