Definition df-pr 3617

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 3686. For a more traditional definition, but requiring a dummy variable, see dfpr2 3629. (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 3611	. 2 class { A , B }
4	1	csn 3610	. . 3 class { A }
5	2	csn 3610	. . 3 class { B }
6	4, 5	cun 3142	. 2 class ( { A } u. { B } )
7	3, 6	wceq 1364	1 wff { A , B } = ( { A } u. { B } )

This definition is referenced by:  dfsn2  3624  dfpr2  3629  ralprg  3661  rexprg  3662  disjpr2  3674  prcom  3686  preq1  3687  qdass  3707  qdassr  3708  tpidm12  3709  prprc1  3718  difprsn1  3749  diftpsn3  3751  difpr  3752  snsspr1  3758  snsspr2  3759  prss  3766  prssg  3767  iunxprg  3985  2ordpr  4544  xpsspw  4759  dmpropg  5122  rnpropg  5129  funprg  5288  funtp  5291  fntpg  5294  f1oprg  5527  fnimapr  5600  fpr  5722  fprg  5723  fmptpr  5732  fvpr1  5744  fvpr1g  5746  fvpr2g  5747  df2o3  6459  enpr2d  6847  unfiexmid  6950  prfidisj  6959  pr2nelem  7225  xp2dju  7249  fzosplitprm1  10271  hashprg  10830  sumpr  11463  strle2g  12631  bdcpr  15127