Metamath Proof Explorer


Theorem foov

Description: An onto mapping of an operation expressed in terms of operation values. (Contributed by NM, 29-Oct-2006)

Ref Expression
Assertion foov F:A×BontoCF:A×BCzCxAyBz=xFy

Proof

Step Hyp Ref Expression
1 dffo3 F:A×BontoCF:A×BCzCwA×Bz=Fw
2 fveq2 w=xyFw=Fxy
3 df-ov xFy=Fxy
4 2 3 eqtr4di w=xyFw=xFy
5 4 eqeq2d w=xyz=Fwz=xFy
6 5 rexxp wA×Bz=FwxAyBz=xFy
7 6 ralbii zCwA×Bz=FwzCxAyBz=xFy
8 7 anbi2i F:A×BCzCwA×Bz=FwF:A×BCzCxAyBz=xFy
9 1 8 bitri F:A×BontoCF:A×BCzCxAyBz=xFy