Definition df-pr 3650

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

This definition is referenced by:  dfsn2  3657  dfpr2  3662  ralprg  3694  rexprg  3695  disjpr2  3707  prcom  3719  preq1  3720  qdass  3740  qdassr  3741  tpidm12  3742  prprc1  3751  difprsn1  3783  diftpsn3  3785  difpr  3786  snsspr1  3792  snsspr2  3793  prss  3800  prssg  3801  iunxprg  4022  2ordpr  4590  xpsspw  4805  dmpropg  5174  rnpropg  5181  funprg  5343  funtp  5346  fntpg  5349  f1oprg  5589  fnimapr  5662  fpr  5789  fprg  5790  fmptpr  5799  fvpr1  5811  fvpr1g  5813  fvpr2g  5814  df2o3  6539  enpr2d  6935  unfiexmid  7041  prfidisj  7050  tpfidceq  7053  pr2nelem  7325  xp2dju  7358  fzosplitprm1  10400  hashprg  10990  sumpr  11839  strle2g  13054  perfectlem2  15587  bdcpr  16006