Definition df-pr 3674

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

This definition is referenced by:  dfsn2  3681  dfpr2  3686  ralprg  3718  rexprg  3719  disjpr2  3731  prcom  3745  preq1  3746  qdass  3766  qdassr  3767  tpidm12  3768  prprc1  3778  difprsn1  3810  diftpsn3  3812  difpr  3813  snsspr1  3819  snsspr2  3820  prss  3827  prssg  3828  iunxprg  4049  2ordpr  4620  xpsspw  4836  dmpropg  5207  rnpropg  5214  funprg  5377  funtp  5380  fntpg  5383  f1oprg  5625  fnimapr  5702  fpr  5831  fprg  5832  fmptpr  5841  fvpr1  5853  fvpr1g  5855  fvpr2g  5856  df2o3  6592  enpr2d  6992  unfiexmid  7103  prfidisj  7112  tpfidceq  7115  pr2nelem  7387  xp2dju  7420  fzosplitpr  10469  fzosplitprm1  10470  hashprg  11062  sumpr  11964  strle2g  13180  perfectlem2  15714  bdcpr  16402