Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > nicbijust  Unicode version 
Description: For nic* definitions, the biconditional connective is not used. Instead, definitions are made based on this form. nicbi1 1459 and nicbi2 1460 are used to convert the definitions into usable theorems about one side of the implication. (Contributed by Jeff Hoffman, 18Nov2007.) (Proof modification is discouraged.) (New usage is discouraged.) 
Ref  Expression 

nicbijust 
Step  Hyp  Ref  Expression 

1  nicswap 1450  1 
Colors of variables: wff set class 
Syntax hints: wnan 1293 
This theorem was proved from axioms: ax1 5 ax2 6 ax3 7 axmp 8 
This theorem depends on definitions: dfbi 178 dfan 361 dfnan 1294 
Copyright terms: Public domain  W3C validator 