Definition df-pr 3716

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

This definition is used by:  dfsn2  3723  dfpr2  3728  ralprg  3760  rexprg  3761  disjpr2  3773  prcom  3787  preq1  3788  qdass  3808  qdassr  3809  tpidm12  3810  prprc1  3821  difprsn1  3854  diftpsn3  3856  difpr  3857  snsspr1  3863  snsspr2  3864  prss  3871  prssg  3872  iunxprg  4093  2ordpr  4673  xpsspw  4889  dmpropg  5263  rnpropg  5270  funprg  5434  funtp  5437  fntpg  5440  f1oprg  5688  fnimapr  5766  fpr  5900  fprg  5901  fmptpr  5910  fvpr1  5922  fvpr1g  5924  fvpr2g  5925  df2o3  6706  enpr2d  7115  unfiexmid  7229  prfidisj  7238  tpfidceq  7241  pr2nelem  7543  xp2dju  7577  fzosplitpr  10669  fzosplitprm1  10670  hashprg  11271  sumpr  12205  strle2g  13520  perfectlem2  16300  bdcpr  17102