Definition df-pr 3625

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

This definition is referenced by:  dfsn2  3632  dfpr2  3637  ralprg  3669  rexprg  3670  disjpr2  3682  prcom  3694  preq1  3695  qdass  3715  qdassr  3716  tpidm12  3717  prprc1  3726  difprsn1  3757  diftpsn3  3759  difpr  3760  snsspr1  3766  snsspr2  3767  prss  3774  prssg  3775  iunxprg  3993  2ordpr  4556  xpsspw  4771  dmpropg  5138  rnpropg  5145  funprg  5304  funtp  5307  fntpg  5310  f1oprg  5544  fnimapr  5617  fpr  5740  fprg  5741  fmptpr  5750  fvpr1  5762  fvpr1g  5764  fvpr2g  5765  df2o3  6483  enpr2d  6871  unfiexmid  6974  prfidisj  6983  pr2nelem  7251  xp2dju  7275  fzosplitprm1  10301  hashprg  10879  sumpr  11556  strle2g  12725  bdcpr  15363