Definition df-pr 3629

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

This definition is referenced by:  dfsn2  3636  dfpr2  3641  ralprg  3673  rexprg  3674  disjpr2  3686  prcom  3698  preq1  3699  qdass  3719  qdassr  3720  tpidm12  3721  prprc1  3730  difprsn1  3761  diftpsn3  3763  difpr  3764  snsspr1  3770  snsspr2  3771  prss  3778  prssg  3779  iunxprg  3997  2ordpr  4560  xpsspw  4775  dmpropg  5142  rnpropg  5149  funprg  5308  funtp  5311  fntpg  5314  f1oprg  5548  fnimapr  5621  fpr  5744  fprg  5745  fmptpr  5754  fvpr1  5766  fvpr1g  5768  fvpr2g  5769  df2o3  6488  enpr2d  6876  unfiexmid  6979  prfidisj  6988  tpfidceq  6991  pr2nelem  7258  xp2dju  7282  fzosplitprm1  10310  hashprg  10900  sumpr  11578  strle2g  12785  perfectlem2  15236  bdcpr  15517