Definition df-pr 3413

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

This definition is referenced by:  dfsn2  3420  dfpr2  3425  ralprg  3451  rexprg  3452  disjpr2  3464  prcom  3476  preq1  3477  qdass  3497  qdassr  3498  tpidm12  3499  prprc1  3508  difprsn1  3533  diftpsn3  3535  snsspr1  3541  snsspr2  3542  prss  3549  prssg  3550  2ordpr  4275  xpsspw  4478  dmpropg  4823  rnpropg  4830  funprg  4980  funtp  4983  fntpg  4986  f1oprg  5199  fnimapr  5265  fpr  5377  fprg  5378  fmptpr  5387  fvpr1  5397  fvpr1g  5399  fvpr2g  5400  df2o3  6078  unfiexmid  6438  pr2nelem  6519  fzosplitprm1  9320  sizeprg  9832  bdcpr  10820