Definition df-pr 3645

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

This definition is referenced by:  dfsn2  3652  dfpr2  3657  ralprg  3689  rexprg  3690  disjpr2  3702  prcom  3714  preq1  3715  qdass  3735  qdassr  3736  tpidm12  3737  prprc1  3746  difprsn1  3778  diftpsn3  3780  difpr  3781  snsspr1  3787  snsspr2  3788  prss  3795  prssg  3796  iunxprg  4017  2ordpr  4585  xpsspw  4800  dmpropg  5169  rnpropg  5176  funprg  5338  funtp  5341  fntpg  5344  f1oprg  5584  fnimapr  5657  fpr  5784  fprg  5785  fmptpr  5794  fvpr1  5806  fvpr1g  5808  fvpr2g  5809  df2o3  6534  enpr2d  6930  unfiexmid  7036  prfidisj  7045  tpfidceq  7048  pr2nelem  7320  xp2dju  7353  fzosplitprm1  10395  hashprg  10985  sumpr  11809  strle2g  13024  perfectlem2  15557  bdcpr  15976