Definition df-pr 3577

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 3646. For a more traditional definition, but requiring a dummy variable, see dfpr2 3589. (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 3571	. 2 class { A , B }
4	1	csn 3570	. . 3 class { A }
5	2	csn 3570	. . 3 class { B }
6	4, 5	cun 3109	. 2 class ( { A } u. { B } )
7	3, 6	wceq 1342	1 wff { A , B } = ( { A } u. { B } )

This definition is referenced by:  dfsn2  3584  dfpr2  3589  ralprg  3621  rexprg  3622  disjpr2  3634  prcom  3646  preq1  3647  qdass  3667  qdassr  3668  tpidm12  3669  prprc1  3678  difprsn1  3706  diftpsn3  3708  difpr  3709  snsspr1  3715  snsspr2  3716  prss  3723  prssg  3724  iunxprg  3940  2ordpr  4495  xpsspw  4710  dmpropg  5070  rnpropg  5077  funprg  5232  funtp  5235  fntpg  5238  f1oprg  5470  fnimapr  5540  fpr  5661  fprg  5662  fmptpr  5671  fvpr1  5683  fvpr1g  5685  fvpr2g  5686  df2o3  6389  enpr2d  6774  unfiexmid  6874  prfidisj  6883  pr2nelem  7138  xp2dju  7162  fzosplitprm1  10159  hashprg  10710  sumpr  11340  strle2g  12422  bdcpr  13588