Definition df-pr 3676

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 3747. For a more traditional definition, but requiring a dummy variable, see dfpr2 3688. (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 3670	. 2 class { A , B }
4	1	csn 3669	. . 3 class { A }
5	2	csn 3669	. . 3 class { B }
6	4, 5	cun 3198	. 2 class ( { A } u. { B } )
7	3, 6	wceq 1397	1 wff { A , B } = ( { A } u. { B } )

This definition is referenced by:  dfsn2  3683  dfpr2  3688  ralprg  3720  rexprg  3721  disjpr2  3733  prcom  3747  preq1  3748  qdass  3768  qdassr  3769  tpidm12  3770  prprc1  3780  difprsn1  3812  diftpsn3  3814  difpr  3815  snsspr1  3821  snsspr2  3822  prss  3829  prssg  3830  iunxprg  4051  2ordpr  4622  xpsspw  4838  dmpropg  5209  rnpropg  5216  funprg  5380  funtp  5383  fntpg  5386  f1oprg  5630  fnimapr  5707  fpr  5837  fprg  5838  fmptpr  5847  fvpr1  5859  fvpr1g  5861  fvpr2g  5862  df2o3  6600  enpr2d  7000  unfiexmid  7113  prfidisj  7122  tpfidceq  7125  pr2nelem  7399  xp2dju  7433  fzosplitpr  10483  fzosplitprm1  10484  hashprg  11076  sumpr  11995  strle2g  13211  perfectlem2  15751  bdcpr  16525