Definition df-pr 4128

Description: Define unordered pair of classes. Definition 7.1 of [Quine] p. 48. For example, 𝐴 ∈ {1, -1} → (𝐴↑2) = 1 (ex-pr 26679). They are unordered, so {𝐴, 𝐵} = {𝐵, 𝐴} as proven by prcom 4211. For a more traditional definition, but requiring a dummy variable, see dfpr2 4143. (Contributed by NM, 21-Jun-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 4127	. 2 class {𝐴, 𝐵}
4	1	csn 4125	. . 3 class {𝐴}
5	2	csn 4125	. . 3 class {𝐵}
6	4, 5	cun 3538	. 2 class ({𝐴} ∪ {𝐵})
7	3, 6	wceq 1475	1 wff {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})

This definition is referenced by:  dfsn2  4138  dfpr2  4143  ralprg  4181  rexprg  4182  csbprg  4191  disjpr2  4194  disjpr2OLD  4195  prcom  4211  preq1  4212  qdass  4232  qdassr  4233  tpidm12  4234  prprc1  4243  difprsn1  4271  diftpsn3OLD  4274  difpr  4275  tpprceq3  4276  snsspr1  4285  snsspr2  4286  prssg  4290  prssOLD  4292  ssunpr  4305  sstp  4307  iunxprg  4543  iunopeqop  4906  pwssun  4944  xpsspw  5156  dmpropg  5526  rnpropg  5533  funprg  5854  funprgOLD  5855  funtp  5859  fntpg  5862  funcnvpr  5864  f1oprswap  6092  f1oprg  6093  fnimapr  6172  residpr  6315  fpr  6326  fmptpr  6343  fvpr1  6361  fvpr1g  6363  fvpr2g  6364  df2o3  7460  map2xp  8015  1sdom  8048  en2  8081  prfi  8120  prwf  8557  rankprb  8597  pr2nelem  8710  xp2cda  8885  ssxr  9986  prunioo  12172  fzosplitprm1  12443  hashprg  13043  hashprgOLD  13044  hashprlei  13107  s2prop  13502  s4prop  13505  f1oun2prg  13512  sumpr  14321  isprm2lem  15232  strlemor2  15797  strle2  15801  phlstr  15857  xpscg  16041  symg2bas  17641  dmdprdpr  18271  dprdpr  18272  lsmpr  18910  lsppr  18914  lspsntri  18918  lsppratlem1  18968  lsppratlem3  18970  lsppratlem4  18971  m2detleib  20256  xpstopnlem1  21422  ovolioo  23143  uniiccdif  23152  i1f1  23263  wilthlem2  24595  perfectlem2  24755  axlowdimlem13  25634  nbgraopALT  25953  constr2spthlem1  26124  constr3pthlem1  26183  constr3pthlem2  26184  ex-dif  26672  ex-un  26673  ex-in  26674  ex-xp  26685  ex-cnv  26686  ex-rn  26689  ex-res  26690  spanpr  27823  superpos  28597  prct  28875  esumpr  29455  eulerpartgbij  29761  signswch  29964  subfacp1lem1  30415  altopthsn  31238  onint1  31618  poimirlem8  32587  poimirlem9  32588  poimirlem15  32594  smprngopr  33021  dihprrnlem1N  35731  dihprrnlem2  35732  djhlsmat  35734  lclkrlem2c  35816  lclkrlem2v  35835  lcfrlem18  35867  dfrcl4  36987  iunrelexp0  37013  corclrcl  37018  corcltrcl  37050  cotrclrcl  37053  sumpair  38217  perfectALTVlem2  40165  rnfdmpr  40325  fzosplitpr  40362  prinfzo0  40363  xpprsng  41903  gsumpr  41932