Definition df-pr 3676

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

This definition is referenced by:  dfsn2  3683  dfpr2  3688  ralprg  3720  rexprg  3721  disjpr2  3733  prcom  3747  preq1  3748  qdass  3768  qdassr  3769  tpidm12  3770  prprc1  3780  difprsn1  3812  diftpsn3  3814  difpr  3815  snsspr1  3821  snsspr2  3822  prss  3829  prssg  3830  iunxprg  4051  2ordpr  4622  xpsspw  4838  dmpropg  5209  rnpropg  5216  funprg  5380  funtp  5383  fntpg  5386  f1oprg  5629  fnimapr  5706  fpr  5835  fprg  5836  fmptpr  5845  fvpr1  5857  fvpr1g  5859  fvpr2g  5860  df2o3  6596  enpr2d  6996  unfiexmid  7109  prfidisj  7118  tpfidceq  7121  pr2nelem  7395  xp2dju  7429  fzosplitpr  10478  fzosplitprm1  10479  hashprg  11071  sumpr  11973  strle2g  13189  perfectlem2  15723  bdcpr  16466