Definition df-pr 3742

Description: Define unordered pair of classes. Definition 7.1 of [Quine] p. 48. For example, A ∈ { 1 , -u 1 } → (A ^ 2 ) = 1 (ex-pr in set.mm). They are unordered, so {A, B} = {B, A} as proven by prcom 3798. For a more traditional definition, but requiring a dummy variable, see dfpr2 3749. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
df-pr	⊢ {A, B} = ({A} ∪ {B})

Detailed syntax breakdown of Definition df-pr

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	cpr 3738	. 2 class {A, B}
4	1	csn 3737	. . 3 class {A}
5	2	csn 3737	. . 3 class {B}
6	4, 5	cun 3207	. 2 class ({A} ∪ {B})
7	3, 6	wceq 1642	1 wff {A, B} = ({A} ∪ {B})

This definition is referenced by:  dfsn2  3747  dfpr2  3749  ralprg  3775  rexprg  3776  prcom  3798  preq1  3799  qdass  3819  qdassr  3820  tpidm12  3821  difprsn1  3847  diftpsn3  3849  snsspr1  3856  snsspr2  3857  prss  3861  prssg  3862  ssunpr  3868  sstp  3870  prex  4112  snprss1  4120  prprc2  4122  dmpropg  5068  funprg  5149  funprgOLD  5150  fnimapr  5374  fpr  5437  fvpr1  5449  1p1e2c  6155  el2c  6191  ce2  6192