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  3967  2ordpr  4523  xpsspw  4738  dmpropg  5101  rnpropg  5108  funprg  5266  funtp  5269  fntpg  5272  f1oprg  5505  fnimapr  5576  fpr  5698  fprg  5699  fmptpr  5708  fvpr1  5720  fvpr1g  5722  fvpr2g  5723  df2o3  6430  enpr2d  6816  unfiexmid  6916  prfidisj  6925  pr2nelem  7189  xp2dju  7213  fzosplitprm1  10233  hashprg  10787  sumpr  11420  strle2g  12565  bdcpr  14593