This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem offveqb

Description: Equivalent expressions for equality with a function operation. (Contributed by NM, 9-Oct-2014) (Proof shortened by Mario Carneiro, 5-Dec-2016)

Ref Expression
Hypotheses offveq.1 
|- ( ph -> A e. V )
offveq.2 
|- ( ph -> F Fn A )
offveq.3 
|- ( ph -> G Fn A )
offveq.4 
|- ( ph -> H Fn A )
offveq.5 
|- ( ( ph /\ x e. A ) -> ( F ` x ) = B )
offveq.6 
|- ( ( ph /\ x e. A ) -> ( G ` x ) = C )
Assertion offveqb 
|- ( ph -> ( H = ( F oF R G ) <-> A. x e. A ( H ` x ) = ( B R C ) ) )

Proof

Step Hyp Ref Expression
1 offveq.1 
 |-  ( ph -> A e. V )
2 offveq.2 
 |-  ( ph -> F Fn A )
3 offveq.3 
 |-  ( ph -> G Fn A )
4 offveq.4 
 |-  ( ph -> H Fn A )
5 offveq.5 
 |-  ( ( ph /\ x e. A ) -> ( F ` x ) = B )
6 offveq.6 
 |-  ( ( ph /\ x e. A ) -> ( G ` x ) = C )
7 dffn5 
 |-  ( H Fn A <-> H = ( x e. A |-> ( H ` x ) ) )
8 4 7 sylib 
 |-  ( ph -> H = ( x e. A |-> ( H ` x ) ) )
9 inidm 
 |-  ( A i^i A ) = A
10 2 3 1 1 9 5 6 offval 
 |-  ( ph -> ( F oF R G ) = ( x e. A |-> ( B R C ) ) )
11 8 10 eqeq12d 
 |-  ( ph -> ( H = ( F oF R G ) <-> ( x e. A |-> ( H ` x ) ) = ( x e. A |-> ( B R C ) ) ) )
12 fvexd 
 |-  ( ph -> ( H ` x ) e. _V )
13 12 ralrimivw 
 |-  ( ph -> A. x e. A ( H ` x ) e. _V )
14 mpteqb 
 |-  ( A. x e. A ( H ` x ) e. _V -> ( ( x e. A |-> ( H ` x ) ) = ( x e. A |-> ( B R C ) ) <-> A. x e. A ( H ` x ) = ( B R C ) ) )
15 13 14 syl 
 |-  ( ph -> ( ( x e. A |-> ( H ` x ) ) = ( x e. A |-> ( B R C ) ) <-> A. x e. A ( H ` x ) = ( B R C ) ) )
16 11 15 bitrd 
 |-  ( ph -> ( H = ( F oF R G ) <-> A. x e. A ( H ` x ) = ( B R C ) ) )