Definition df-pr 3639

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

This definition is referenced by:  dfsn2  3646  dfpr2  3651  ralprg  3683  rexprg  3684  disjpr2  3696  prcom  3708  preq1  3709  qdass  3729  qdassr  3730  tpidm12  3731  prprc1  3740  difprsn1  3771  diftpsn3  3773  difpr  3774  snsspr1  3780  snsspr2  3781  prss  3788  prssg  3789  iunxprg  4007  2ordpr  4571  xpsspw  4786  dmpropg  5154  rnpropg  5161  funprg  5323  funtp  5326  fntpg  5329  f1oprg  5565  fnimapr  5638  fpr  5765  fprg  5766  fmptpr  5775  fvpr1  5787  fvpr1g  5789  fvpr2g  5790  df2o3  6515  enpr2d  6910  unfiexmid  7014  prfidisj  7023  tpfidceq  7026  pr2nelem  7298  xp2dju  7326  fzosplitprm1  10361  hashprg  10951  sumpr  11695  strle2g  12910  perfectlem2  15443  bdcpr  15769