Definition df-pr 3590

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 3659. For a more traditional definition, but requiring a dummy variable, see dfpr2 3602. (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 3584	. 2 class { A , B }
4	1	csn 3583	. . 3 class { A }
5	2	csn 3583	. . 3 class { B }
6	4, 5	cun 3119	. 2 class ( { A } u. { B } )
7	3, 6	wceq 1348	1 wff { A , B } = ( { A } u. { B } )

This definition is referenced by:  dfsn2  3597  dfpr2  3602  ralprg  3634  rexprg  3635  disjpr2  3647  prcom  3659  preq1  3660  qdass  3680  qdassr  3681  tpidm12  3682  prprc1  3691  difprsn1  3719  diftpsn3  3721  difpr  3722  snsspr1  3728  snsspr2  3729  prss  3736  prssg  3737  iunxprg  3953  2ordpr  4508  xpsspw  4723  dmpropg  5083  rnpropg  5090  funprg  5248  funtp  5251  fntpg  5254  f1oprg  5486  fnimapr  5556  fpr  5678  fprg  5679  fmptpr  5688  fvpr1  5700  fvpr1g  5702  fvpr2g  5703  df2o3  6409  enpr2d  6795  unfiexmid  6895  prfidisj  6904  pr2nelem  7168  xp2dju  7192  fzosplitprm1  10190  hashprg  10743  sumpr  11376  strle2g  12509  bdcpr  13906