Theorem bnj1234

Description: Technical lemma for bnj60 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj1234.2	|- Y = <. x , ( f |` _pred ( x , A , R ) ) >.
	bnj1234.3	|- C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
	bnj1234.4	|- Z = <. x , ( g |` _pred ( x , A , R ) ) >.
	bnj1234.5	|- D = { g | E. d e. B ( g Fn d /\ A. x e. d ( g ` x ) = ( G ` Z ) ) }
Assertion	bnj1234	|- C = D

Proof

Step	Hyp	Ref	Expression
1		bnj1234.2	|- Y = <. x , ( f |` _pred ( x , A , R ) ) >.
2		bnj1234.3	|- C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
3		bnj1234.4	|- Z = <. x , ( g |` _pred ( x , A , R ) ) >.
4		bnj1234.5	|- D = { g | E. d e. B ( g Fn d /\ A. x e. d ( g ` x ) = ( G ` Z ) ) }
5		fneq1	|- ( f = g -> ( f Fn d <-> g Fn d ) )
6		fveq1	|- ( f = g -> ( f ` x ) = ( g ` x ) )
7		reseq1	|- ( f = g -> ( f |` _pred ( x , A , R ) ) = ( g |` _pred ( x , A , R ) ) )
8	7	opeq2d	|- ( f = g -> <. x , ( f |` _pred ( x , A , R ) ) >. = <. x , ( g |` _pred ( x , A , R ) ) >. )
9	8 1 3	3eqtr4g	|- ( f = g -> Y = Z )
10	9	fveq2d	|- ( f = g -> ( G ` Y ) = ( G ` Z ) )
11	6 10	eqeq12d	|- ( f = g -> ( ( f ` x ) = ( G ` Y ) <-> ( g ` x ) = ( G ` Z ) ) )
12	11	ralbidv	|- ( f = g -> ( A. x e. d ( f ` x ) = ( G ` Y ) <-> A. x e. d ( g ` x ) = ( G ` Z ) ) )
13	5 12	anbi12d	|- ( f = g -> ( ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) <-> ( g Fn d /\ A. x e. d ( g ` x ) = ( G ` Z ) ) ) )
14	13	rexbidv	|- ( f = g -> ( E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) <-> E. d e. B ( g Fn d /\ A. x e. d ( g ` x ) = ( G ` Z ) ) ) )
15	14	cbvabv	|- { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) } = { g | E. d e. B ( g Fn d /\ A. x e. d ( g ` x ) = ( G ` Z ) ) }
16	15 2 4	3eqtr4i	|- C = D