Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > wf1o  Unicode version 
Description: Extend the definition of a wff to include onetoone onto functions. (Read: maps onetoone onto .) The notation ("11" above the arrow and "onto" below the arrow) is from Definition 6.15(6) of [TakeutiZaring] p. 27. 
Ref  Expression 

cA  
cB  
cF 
Ref  Expression 

wf1o 
Colors of variables: wff setvar class 
Copyright terms: Public domain  W3C validator 