Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > nicbijust  Structured version Unicode version 
Description: For nic* definitions, the biconditional connective is not used. Instead, definitions are made based on this form. nicbi1 1462 and nicbi2 1463 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 1453  1 
Colors of variables: wff set class 
Syntax hints: wnan 1296 
This theorem was proved from axioms: ax1 5 ax2 6 ax3 7 axmp 8 
This theorem depends on definitions: dfbi 178 dfan 361 dfnan 1297 
Copyright terms: Public domain  W3C validator 