Definition df-pr 3680

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

This definition is referenced by:  dfsn2  3687  dfpr2  3692  ralprg  3724  rexprg  3725  disjpr2  3737  prcom  3751  preq1  3752  qdass  3772  qdassr  3773  tpidm12  3774  prprc1  3784  difprsn1  3817  diftpsn3  3819  difpr  3820  snsspr1  3826  snsspr2  3827  prss  3834  prssg  3835  iunxprg  4056  2ordpr  4628  xpsspw  4844  dmpropg  5216  rnpropg  5223  funprg  5387  funtp  5390  fntpg  5393  f1oprg  5638  fnimapr  5715  fpr  5844  fprg  5845  fmptpr  5854  fvpr1  5866  fvpr1g  5868  fvpr2g  5869  df2o3  6640  enpr2d  7040  unfiexmid  7153  prfidisj  7162  tpfidceq  7165  pr2nelem  7456  xp2dju  7490  fzosplitpr  10542  fzosplitprm1  10543  hashprg  11135  sumpr  12054  strle2g  13270  perfectlem2  15814  bdcpr  16587