Definition df-pr 3698

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

This definition is referenced by:  dfsn2  3705  dfpr2  3710  ralprg  3742  rexprg  3743  disjpr2  3755  prcom  3769  preq1  3770  qdass  3790  qdassr  3791  tpidm12  3792  prprc1  3802  difprsn1  3835  diftpsn3  3837  difpr  3838  snsspr1  3844  snsspr2  3845  prss  3852  prssg  3853  iunxprg  4074  2ordpr  4648  xpsspw  4864  dmpropg  5237  rnpropg  5244  funprg  5408  funtp  5411  fntpg  5414  f1oprg  5662  fnimapr  5739  fpr  5868  fprg  5869  fmptpr  5878  fvpr1  5890  fvpr1g  5892  fvpr2g  5893  df2o3  6664  enpr2d  7066  unfiexmid  7180  prfidisj  7189  tpfidceq  7192  pr2nelem  7490  xp2dju  7524  fzosplitpr  10583  fzosplitprm1  10584  hashprg  11177  sumpr  12103  strle2g  13337  perfectlem2  15885  bdcpr  16658