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  5629  fnimapr  5706  fpr  5836  fprg  5837  fmptpr  5846  fvpr1  5858  fvpr1g  5860  fvpr2g  5861  df2o3  6597  enpr2d  6997  unfiexmid  7110  prfidisj  7119  tpfidceq  7122  pr2nelem  7396  xp2dju  7430  fzosplitpr  10480  fzosplitprm1  10481  hashprg  11073  sumpr  11976  strle2g  13192  perfectlem2  15727  bdcpr  16483