Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

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

cA  
cB  
cF 
Ref  Expression 

wf1 
Colors of variables: wff set class 
Copyright terms: Public domain  W3C validator 