Definition df-pr 3599

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

This definition is referenced by:  dfsn2  3606  dfpr2  3611  ralprg  3643  rexprg  3644  disjpr2  3656  prcom  3668  preq1  3669  qdass  3689  qdassr  3690  tpidm12  3691  prprc1  3700  difprsn1  3731  diftpsn3  3733  difpr  3734  snsspr1  3740  snsspr2  3741  prss  3748  prssg  3749  iunxprg  3965  2ordpr  4521  xpsspw  4736  dmpropg  5098  rnpropg  5105  funprg  5263  funtp  5266  fntpg  5269  f1oprg  5502  fnimapr  5573  fpr  5695  fprg  5696  fmptpr  5705  fvpr1  5717  fvpr1g  5719  fvpr2g  5720  df2o3  6426  enpr2d  6812  unfiexmid  6912  prfidisj  6921  pr2nelem  7185  xp2dju  7209  fzosplitprm1  10227  hashprg  10779  sumpr  11412  strle2g  12556  bdcpr  14394