Definition df-pr 3534

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 3599. For a more traditional definition, but requiring a dummy variable, see dfpr2 3546. (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 3528	. 2 class { A , B }
4	1	csn 3527	. . 3 class { A }
5	2	csn 3527	. . 3 class { B }
6	4, 5	cun 3069	. 2 class ( { A } u. { B } )
7	3, 6	wceq 1331	1 wff { A , B } = ( { A } u. { B } )

This definition is referenced by:  dfsn2  3541  dfpr2  3546  ralprg  3574  rexprg  3575  disjpr2  3587  prcom  3599  preq1  3600  qdass  3620  qdassr  3621  tpidm12  3622  prprc1  3631  difprsn1  3659  diftpsn3  3661  difpr  3662  snsspr1  3668  snsspr2  3669  prss  3676  prssg  3677  iunxprg  3893  2ordpr  4439  xpsspw  4651  dmpropg  5011  rnpropg  5018  funprg  5173  funtp  5176  fntpg  5179  f1oprg  5411  fnimapr  5481  fpr  5602  fprg  5603  fmptpr  5612  fvpr1  5624  fvpr1g  5626  fvpr2g  5627  df2o3  6327  enpr2d  6711  unfiexmid  6806  prfidisj  6815  pr2nelem  7047  xp2dju  7071  fzosplitprm1  10011  hashprg  10554  sumpr  11182  strle2g  12050  bdcpr  13069