Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > re1luk1  Unicode version 
Description: luk1 1426 derived from the TarskiBernaysWajsberg axioms. (Contributed by Anthony Hart, 16Aug2011.) (Proof modification is discouraged.) (New usage is discouraged.) 
Ref  Expression 

re1luk1 
Step  Hyp  Ref  Expression 

1  tbwax1 1471  1 
Colors of variables: wff set class 
Syntax hints: wi 4 
This theorem was proved from axioms: ax1 5 ax2 6 axmp 8 
Copyright terms: Public domain  W3C validator 