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

Metamath Proof Explorer

Theorem bnj1234

Proof