Definition df-pr 3405

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

This definition is referenced by:  dfsn2  3412  dfpr2  3417  ralprg  3443  rexprg  3444  disjpr2  3456  prcom  3468  preq1  3469  qdass  3489  qdassr  3490  tpidm12  3491  prprc1  3500  difprsn1  3525  diftpsn3  3527  snsspr1  3533  snsspr2  3534  prss  3541  prssg  3542  2ordpr  4267  xpsspw  4468  dmpropg  4813  rnpropg  4820  funprg  4969  funtp  4972  fntpg  4975  f1oprg  5188  fnimapr  5254  fpr  5366  fprg  5367  fmptpr  5376  fvpr1  5386  fvpr1g  5388  fvpr2g  5389  df2o3  6037  pr2nelem  6460  fzosplitprm1  9243  bdcpr  10662