ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-pr GIF version

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

Detailed syntax breakdown of Definition df-pr
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
31, 2cpr 3533 . 2 class {𝐴, 𝐵}
41csn 3532 . . 3 class {𝐴}
52csn 3532 . . 3 class {𝐵}
64, 5cun 3074 . 2 class ({𝐴} ∪ {𝐵})
73, 6wceq 1332 1 wff {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})
Colors of variables: wff set class
This definition is referenced by:  dfsn2  3546  dfpr2  3551  ralprg  3582  rexprg  3583  disjpr2  3595  prcom  3607  preq1  3608  qdass  3628  qdassr  3629  tpidm12  3630  prprc1  3639  difprsn1  3667  diftpsn3  3669  difpr  3670  snsspr1  3676  snsspr2  3677  prss  3684  prssg  3685  iunxprg  3901  2ordpr  4447  xpsspw  4659  dmpropg  5019  rnpropg  5026  funprg  5181  funtp  5184  fntpg  5187  f1oprg  5419  fnimapr  5489  fpr  5610  fprg  5611  fmptpr  5620  fvpr1  5632  fvpr1g  5634  fvpr2g  5635  df2o3  6335  enpr2d  6719  unfiexmid  6814  prfidisj  6823  pr2nelem  7064  xp2dju  7088  fzosplitprm1  10042  hashprg  10586  sumpr  11214  strle2g  12089  bdcpr  13240
  Copyright terms: Public domain W3C validator