Definition df-pr 3481

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

This definition is referenced by:  dfsn2  3488  dfpr2  3493  ralprg  3521  rexprg  3522  disjpr2  3534  prcom  3546  preq1  3547  qdass  3567  qdassr  3568  tpidm12  3569  prprc1  3578  difprsn1  3606  diftpsn3  3608  difpr  3609  snsspr1  3615  snsspr2  3616  prss  3623  prssg  3624  2ordpr  4377  xpsspw  4589  dmpropg  4947  rnpropg  4954  funprg  5109  funtp  5112  fntpg  5115  f1oprg  5343  fnimapr  5413  fpr  5534  fprg  5535  fmptpr  5544  fvpr1  5556  fvpr1g  5558  fvpr2g  5559  df2o3  6257  unfiexmid  6735  prfidisj  6744  pr2nelem  6958  xp2dju  6975  fzosplitprm1  9852  hashprg  10395  sumpr  11021  strle2g  11832  bdcpr  12650