Definition df-pr 3596

Description: Define unordered pair of classes. Definition 7.1 of [Quine] p. 48. They are unordered, so { A , B } = { B , A } as proven by prcom 3665. For a more traditional definition, but requiring a dummy variable, see dfpr2 3608. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
df-pr	|- { A , B } = ( { A } u. { 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 3590	. 2 class { A , B }
4	1	csn 3589	. . 3 class { A }
5	2	csn 3589	. . 3 class { B }
6	4, 5	cun 3125	. 2 class ( { A } u. { B } )
7	3, 6	wceq 1353	1 wff { A , B } = ( { A } u. { B } )

This definition is referenced by:  dfsn2  3603  dfpr2  3608  ralprg  3640  rexprg  3641  disjpr2  3653  prcom  3665  preq1  3666  qdass  3686  qdassr  3687  tpidm12  3688  prprc1  3697  difprsn1  3728  diftpsn3  3730  difpr  3731  snsspr1  3737  snsspr2  3738  prss  3745  prssg  3746  iunxprg  3962  2ordpr  4517  xpsspw  4732  dmpropg  5093  rnpropg  5100  funprg  5258  funtp  5261  fntpg  5264  f1oprg  5497  fnimapr  5568  fpr  5690  fprg  5691  fmptpr  5700  fvpr1  5712  fvpr1g  5714  fvpr2g  5715  df2o3  6421  enpr2d  6807  unfiexmid  6907  prfidisj  6916  pr2nelem  7180  xp2dju  7204  fzosplitprm1  10204  hashprg  10756  sumpr  11389  strle2g  12531  bdcpr  14192