Definition df-pr 3626

Description: Define unordered pair of classes. Definition 7.1 of [Quine] p. 48. They are unordered, so {𝐴, 𝐵} = {𝐵, 𝐴} as proven by prcom 3695. For a more traditional definition, but requiring a dummy variable, see dfpr2 3638. (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 3620	. 2 class {𝐴, 𝐵}
4	1	csn 3619	. . 3 class {𝐴}
5	2	csn 3619	. . 3 class {𝐵}
6	4, 5	cun 3152	. 2 class ({𝐴} ∪ {𝐵})
7	3, 6	wceq 1364	1 wff {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})

This definition is referenced by:  dfsn2  3633  dfpr2  3638  ralprg  3670  rexprg  3671  disjpr2  3683  prcom  3695  preq1  3696  qdass  3716  qdassr  3717  tpidm12  3718  prprc1  3727  difprsn1  3758  diftpsn3  3760  difpr  3761  snsspr1  3767  snsspr2  3768  prss  3775  prssg  3776  iunxprg  3994  2ordpr  4557  xpsspw  4772  dmpropg  5139  rnpropg  5146  funprg  5305  funtp  5308  fntpg  5311  f1oprg  5545  fnimapr  5618  fpr  5741  fprg  5742  fmptpr  5751  fvpr1  5763  fvpr1g  5765  fvpr2g  5766  df2o3  6485  enpr2d  6873  unfiexmid  6976  prfidisj  6985  pr2nelem  7253  xp2dju  7277  fzosplitprm1  10304  hashprg  10882  sumpr  11559  strle2g  12728  bdcpr  15433