Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-altop Structured version   Visualization version   GIF version

Definition df-altop 32392
Description: An alternative definition of ordered pairs. This definition removes a hypothesis from its defining theorem (see altopth 32403), making it more convenient in some circumstances. (Contributed by Scott Fenton, 22-Mar-2012.)
Assertion
Ref Expression
df-altop 𝐴, 𝐵⟫ = {{𝐴}, {𝐴, {𝐵}}}

Detailed syntax breakdown of Definition df-altop
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
31, 2caltop 32390 . 2 class 𝐴, 𝐵
41csn 4321 . . 3 class {𝐴}
52csn 4321 . . . 4 class {𝐵}
61, 5cpr 4323 . . 3 class {𝐴, {𝐵}}
74, 6cpr 4323 . 2 class {{𝐴}, {𝐴, {𝐵}}}
83, 7wceq 1632 1 wff 𝐴, 𝐵⟫ = {{𝐴}, {𝐴, {𝐵}}}
Colors of variables: wff setvar class
This definition is referenced by:  altopex  32394  altopthsn  32395  altxpsspw  32411  rankaltopb  32413  nfaltop  32414
  Copyright terms: Public domain W3C validator