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=xf↾predxAR
bnj1234.3 ⊢C=f|∃d∈BfFnd∧∀x∈df⁡x=G⁡Y
bnj1234.4 ⊢Z=xg↾predxAR
bnj1234.5 ⊢D=g|∃d∈BgFnd∧∀x∈dg⁡x=G⁡Z
Assertion bnj1234 ⊢C=D

Proof

Step Hyp Ref Expression
1 bnj1234.2 ⊢Y=xf↾predxAR
2 bnj1234.3 ⊢C=f|∃d∈BfFnd∧∀x∈df⁡x=G⁡Y
3 bnj1234.4 ⊢Z=xg↾predxAR
4 bnj1234.5 ⊢D=g|∃d∈BgFnd∧∀x∈dg⁡x=G⁡Z
5 fneq1 ⊢f=g→fFnd↔gFnd
6 fveq1 ⊢f=g→f⁡x=g⁡x
7 reseq1 ⊢f=g→f↾predxAR=g↾predxAR
8 7 opeq2d ⊢f=g→xf↾predxAR=xg↾predxAR
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→∀x∈df⁡x=G⁡Y↔∀x∈dg⁡x=G⁡Z
13 5 12 anbi12d ⊢f=g→fFnd∧∀x∈df⁡x=G⁡Y↔gFnd∧∀x∈dg⁡x=G⁡Z
14 13 rexbidv ⊢f=g→∃d∈BfFnd∧∀x∈df⁡x=G⁡Y↔∃d∈BgFnd∧∀x∈dg⁡x=G⁡Z
15 14 cbvabv ⊢f|∃d∈BfFnd∧∀x∈df⁡x=G⁡Y=g|∃d∈BgFnd∧∀x∈dg⁡x=G⁡Z
16 15 2 4 3eqtr4i ⊢C=D