Definition df-pr 3614

Description: Define unordered pair of classes. Definition 7.1 of [Quine] p. 48. They are unordered, so {𝐴, 𝐵} = {𝐵, 𝐴} as proven by prcom 3683. For a more traditional definition, but requiring a dummy variable, see dfpr2 3626. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
df-pr	⊢ {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})

Detailed syntax breakdown of Definition df-pr

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3	1, 2	cpr 3608	. 2 class {𝐴, 𝐵}
4	1	csn 3607	. . 3 class {𝐴}
5	2	csn 3607	. . 3 class {𝐵}
6	4, 5	cun 3142	. 2 class ({𝐴} ∪ {𝐵})
7	3, 6	wceq 1364	1 wff {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})

This definition is referenced by:  dfsn2  3621  dfpr2  3626  ralprg  3658  rexprg  3659  disjpr2  3671  prcom  3683  preq1  3684  qdass  3704  qdassr  3705  tpidm12  3706  prprc1  3715  difprsn1  3746  diftpsn3  3748  difpr  3749  snsspr1  3755  snsspr2  3756  prss  3763  prssg  3764  iunxprg  3982  2ordpr  4541  xpsspw  4756  dmpropg  5119  rnpropg  5126  funprg  5285  funtp  5288  fntpg  5291  f1oprg  5524  fnimapr  5597  fpr  5719  fprg  5720  fmptpr  5729  fvpr1  5741  fvpr1g  5743  fvpr2g  5744  df2o3  6456  enpr2d  6844  unfiexmid  6947  prfidisj  6956  pr2nelem  7221  xp2dju  7245  fzosplitprm1  10266  hashprg  10823  sumpr  11456  strle2g  12622  bdcpr  15101