Definition df-pr 3673

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

This definition is referenced by:  dfsn2  3680  dfpr2  3685  ralprg  3717  rexprg  3718  disjpr2  3730  prcom  3742  preq1  3743  qdass  3763  qdassr  3764  tpidm12  3765  prprc1  3774  difprsn1  3806  diftpsn3  3808  difpr  3809  snsspr1  3815  snsspr2  3816  prss  3823  prssg  3824  iunxprg  4045  2ordpr  4615  xpsspw  4830  dmpropg  5200  rnpropg  5207  funprg  5370  funtp  5373  fntpg  5376  f1oprg  5616  fnimapr  5693  fpr  5820  fprg  5821  fmptpr  5830  fvpr1  5842  fvpr1g  5844  fvpr2g  5845  df2o3  6574  enpr2d  6970  unfiexmid  7076  prfidisj  7085  tpfidceq  7088  pr2nelem  7360  xp2dju  7393  fzosplitprm1  10435  hashprg  11025  sumpr  11919  strle2g  13135  perfectlem2  15668  bdcpr  16192