Definition df-pr 3716

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 3787. For a more traditional definition, but requiring a dummy variable, see dfpr2 3728. (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 3710	. 2 class { A , B }
4	1	csn 3709	. . 3 class { A }
5	2	csn 3709	. . 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 used by:  dfsn2  3723  dfpr2  3728  ralprg  3760  rexprg  3761  disjpr2  3773  prcom  3787  preq1  3788  qdass  3808  qdassr  3809  tpidm12  3810  prprc1  3821  difprsn1  3854  diftpsn3  3856  difpr  3857  snsspr1  3863  snsspr2  3864  prss  3871  prssg  3872  iunxprg  4093  2ordpr  4673  xpsspw  4889  dmpropg  5263  rnpropg  5270  funprg  5434  funtp  5437  fntpg  5440  f1oprg  5688  fnimapr  5766  fpr  5900  fprg  5901  fmptpr  5910  fvpr1  5922  fvpr1g  5924  fvpr2g  5925  df2o3  6706  enpr2d  7116  unfiexmid  7230  prfidisj  7239  tpfidceq  7242  pr2nelem  7544  xp2dju  7578  fzosplitpr  10670  fzosplitprm1  10671  hashprg  11272  sumpr  12206  strle2g  13521  perfectlem2  16312  bdcpr  17114