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 ) ) )