Metamath Proof Explorer


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=xfpredxAR
bnj1234.3 C=f|dBfFndxdfx=GY
bnj1234.4 Z=xgpredxAR
bnj1234.5 D=g|dBgFndxdgx=GZ
Assertion bnj1234 C=D

Proof

Step Hyp Ref Expression
1 bnj1234.2 Y=xfpredxAR
2 bnj1234.3 C=f|dBfFndxdfx=GY
3 bnj1234.4 Z=xgpredxAR
4 bnj1234.5 D=g|dBgFndxdgx=GZ
5 fneq1 f=gfFndgFnd
6 fveq1 f=gfx=gx
7 reseq1 f=gfpredxAR=gpredxAR
8 7 opeq2d f=gxfpredxAR=xgpredxAR
9 8 1 3 3eqtr4g f=gY=Z
10 9 fveq2d f=gGY=GZ
11 6 10 eqeq12d f=gfx=GYgx=GZ
12 11 ralbidv f=gxdfx=GYxdgx=GZ
13 5 12 anbi12d f=gfFndxdfx=GYgFndxdgx=GZ
14 13 rexbidv f=gdBfFndxdfx=GYdBgFndxdgx=GZ
15 14 cbvabv f|dBfFndxdfx=GY=g|dBgFndxdgx=GZ
16 15 2 4 3eqtr4i C=D