Metamath Proof Explorer

Theorem funoprabg

Description: "At most one" is a sufficient condition for an operation class abstraction to be a function. (Contributed by NM, 28-Aug-2007)

Ref Expression
Assertion funoprabg 
|- ( A. x A. y E* z ph -> Fun { <. <. x , y >. , z >. | ph } )

Proof

Step Hyp Ref Expression
1 mosubopt 
 |-  ( A. x A. y E* z ph -> E* z E. x E. y ( w = <. x , y >. /\ ph ) )
2 1 alrimiv 
 |-  ( A. x A. y E* z ph -> A. w E* z E. x E. y ( w = <. x , y >. /\ ph ) )
3 dfoprab2 
 |-  { <. <. x , y >. , z >. | ph } = { <. w , z >. | E. x E. y ( w = <. x , y >. /\ ph ) }
4 3 funeqi 
 |-  ( Fun { <. <. x , y >. , z >. | ph } <-> Fun { <. w , z >. | E. x E. y ( w = <. x , y >. /\ ph ) } )
5 funopab 
 |-  ( Fun { <. w , z >. | E. x E. y ( w = <. x , y >. /\ ph ) } <-> A. w E* z E. x E. y ( w = <. x , y >. /\ ph ) )
6 4 5 bitr2i 
 |-  ( A. w E* z E. x E. y ( w = <. x , y >. /\ ph ) <-> Fun { <. <. x , y >. , z >. | ph } )
7 2 6 sylib 
 |-  ( A. x A. y E* z ph -> Fun { <. <. x , y >. , z >. | ph } )