Definition df-pr 3630

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

This definition is referenced by:  dfsn2  3637  dfpr2  3642  ralprg  3674  rexprg  3675  disjpr2  3687  prcom  3699  preq1  3700  qdass  3720  qdassr  3721  tpidm12  3722  prprc1  3731  difprsn1  3762  diftpsn3  3764  difpr  3765  snsspr1  3771  snsspr2  3772  prss  3779  prssg  3780  iunxprg  3998  2ordpr  4561  xpsspw  4776  dmpropg  5143  rnpropg  5150  funprg  5309  funtp  5312  fntpg  5315  f1oprg  5551  fnimapr  5624  fpr  5747  fprg  5748  fmptpr  5757  fvpr1  5769  fvpr1g  5771  fvpr2g  5772  df2o3  6497  enpr2d  6885  unfiexmid  6988  prfidisj  6997  tpfidceq  7000  pr2nelem  7272  xp2dju  7300  fzosplitprm1  10329  hashprg  10919  sumpr  11597  strle2g  12812  perfectlem2  15344  bdcpr  15625