Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-bis Unicode version

Definition df-bis 26020
Description: Definition of the symbol  <->. Experimental. (Contributed by FL, 2-Feb-2014.)
Assertion
Ref Expression
df-bis  |-  <=> c  =  { <. 1 ,  5 >. }

Detailed syntax breakdown of Definition df-bis
StepHypRef Expression
1 cbis 26019 . 2  class  <=> c
2 c1 8738 . . . 4  class  1
3 c5 9798 . . . 4  class  5
42, 3cop 3643 . . 3  class  <. 1 ,  5 >.
54csn 3640 . 2  class  { <. 1 ,  5 >. }
61, 5wceq 1623 1  wff  <=> c  =  { <. 1 ,  5 >. }
Colors of variables: wff set class
This definition is referenced by:  fnckle  26045
  Copyright terms: Public domain W3C validator