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  4671  xpsspw  4887  dmpropg  5260  rnpropg  5267  funprg  5431  funtp  5434  fntpg  5437  f1oprg  5685  fnimapr  5763  fpr  5897  fprg  5898  fmptpr  5907  fvpr1  5919  fvpr1g  5921  fvpr2g  5922  df2o3  6702  enpr2d  7111  unfiexmid  7225  prfidisj  7234  tpfidceq  7237  pr2nelem  7537  xp2dju  7571  fzosplitpr  10652  fzosplitprm1  10653  hashprg  11249  sumpr  12180  strle2g  13461  perfectlem2  16114  bdcpr  16897