Definition df-pr 3673

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 3742. For a more traditional definition, but requiring a dummy variable, see dfpr2 3685. (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 3667	. 2 class { A , B }
4	1	csn 3666	. . 3 class { A }
5	2	csn 3666	. . 3 class { B }
6	4, 5	cun 3195	. 2 class ( { A } u. { B } )
7	3, 6	wceq 1395	1 wff { A , B } = ( { A } u. { B } )

This definition is referenced by:  dfsn2  3680  dfpr2  3685  ralprg  3717  rexprg  3718  disjpr2  3730  prcom  3742  preq1  3743  qdass  3763  qdassr  3764  tpidm12  3765  prprc1  3775  difprsn1  3807  diftpsn3  3809  difpr  3810  snsspr1  3816  snsspr2  3817  prss  3824  prssg  3825  iunxprg  4046  2ordpr  4616  xpsspw  4831  dmpropg  5201  rnpropg  5208  funprg  5371  funtp  5374  fntpg  5377  f1oprg  5617  fnimapr  5694  fpr  5821  fprg  5822  fmptpr  5831  fvpr1  5843  fvpr1g  5845  fvpr2g  5846  df2o3  6576  enpr2d  6972  unfiexmid  7080  prfidisj  7089  tpfidceq  7092  pr2nelem  7364  xp2dju  7397  fzosplitprm1  10440  hashprg  11030  sumpr  11924  strle2g  13140  perfectlem2  15674  bdcpr  16234