Definition df-pr 3715

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

This definition is referenced by:  dfsn2  3722  dfpr2  3727  ralprg  3759  rexprg  3760  disjpr2  3772  prcom  3786  preq1  3787  qdass  3807  qdassr  3808  tpidm12  3809  prprc1  3819  difprsn1  3852  diftpsn3  3854  difpr  3855  snsspr1  3861  snsspr2  3862  prss  3869  prssg  3870  iunxprg  4091  2ordpr  4669  xpsspw  4885  dmpropg  5258  rnpropg  5265  funprg  5429  funtp  5432  fntpg  5435  f1oprg  5683  fnimapr  5760  fpr  5891  fprg  5892  fmptpr  5901  fvpr1  5913  fvpr1g  5915  fvpr2g  5916  df2o3  6695  enpr2d  7104  unfiexmid  7218  prfidisj  7227  tpfidceq  7230  pr2nelem  7530  xp2dju  7564  fzosplitpr  10633  fzosplitprm1  10634  hashprg  11230  sumpr  12161  strle2g  13441  perfectlem2  16031  bdcpr  16814