Definition df-pr 3715

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 3786. For a more traditional definition, but requiring a dummy variable, see dfpr2 3727. (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 3709	. 2 class { A , B }
4	1	csn 3708	. . 3 class { A }
5	2	csn 3708	. . 3 class { B }
6	4, 5	cun 3218	. 2 class ( { A } u. { B } )
7	3, 6	wceq 1402	1 wff { A , B } = ( { A } u. { B } )

This definition is referenced by:  dfsn2  3722  dfpr2  3727  ralprg  3759  rexprg  3760  disjpr2  3772  prcom  3786  preq1  3787  qdass  3807  qdassr  3808  tpidm12  3809  prprc1  3819  difprsn1  3852  diftpsn3  3854  difpr  3855  snsspr1  3861  snsspr2  3862  prss  3869  prssg  3870  iunxprg  4091  2ordpr  4669  xpsspw  4885  dmpropg  5258  rnpropg  5265  funprg  5429  funtp  5432  fntpg  5435  f1oprg  5683  fnimapr  5760  fpr  5891  fprg  5892  fmptpr  5901  fvpr1  5913  fvpr1g  5915  fvpr2g  5916  df2o3  6696  enpr2d  7105  unfiexmid  7219  prfidisj  7228  tpfidceq  7231  pr2nelem  7531  xp2dju  7565  fzosplitpr  10635  fzosplitprm1  10636  hashprg  11232  sumpr  12163  strle2g  13444  perfectlem2  16097  bdcpr  16880