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

Definition df-altop 29173
Description: An alternative definition of ordered pairs. This definition removes a hypothesis from its defining theorem (see altopth 29184), making it more convenient in some circumstances. (Contributed by Scott Fenton, 22-Mar-2012.)
Assertion
Ref Expression
df-altop  |-  << A ,  B >>  =  { { A } ,  { A ,  { B } } }

Detailed syntax breakdown of Definition df-altop
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
31, 2caltop 29171 . 2  class  << A ,  B >>
41csn 4022 . . 3  class  { A }
52csn 4022 . . . 4  class  { B }
61, 5cpr 4024 . . 3  class  { A ,  { B } }
74, 6cpr 4024 . 2  class  { { A } ,  { A ,  { B } } }
83, 7wceq 1374 1  wff  << A ,  B >>  =  { { A } ,  { A ,  { B } } }
Colors of variables: wff setvar class
This definition is referenced by:  altopex  29175  altopthsn  29176  altxpsspw  29192  rankaltopb  29194  nfaltop  29195
  Copyright terms: Public domain W3C validator