Theorem bnj984 13358

Description: Technical lemma of bnj69 13455. 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).

Hypotheses

Ref	Expression
bnj984.3	|- (ch <-> (n e. D /\ f Fn n /\ ph /\ ps))
bnj984.11	|- B = {f | E.n e. D (f Fn n /\ ph /\ ps)}

Assertion

Ref	Expression
bnj984	|- (G e. A -> (G e. B <-> [G / f]E.nch))

Proof of Theorem bnj984

Step	Hyp	Ref	Expression
1		elabsg 2488	. . 3 |- (G e. A -> (G e. {f | E.n e. D (f Fn n /\ ph /\ ps)} <-> [G / f]E.n e. D (f Fn n /\ ph /\ ps)))
2		bnj984.11	. . . 4 |- B = {f | E.n e. D (f Fn n /\ ph /\ ps)}
3	2	eleq2i 1961	. . 3 |- (G e. B <-> G e. {f | E.n e. D (f Fn n /\ ph /\ ps)})
4	1, 3	syl5bb 591	. 2 |- (G e. A -> (G e. B <-> [G / f]E.n e. D (f Fn n /\ ph /\ ps)))
5		df-rex 2110	. . . 4 |- (E.n e. D (f Fn n /\ ph /\ ps) <-> E.n(n e. D /\ (f Fn n /\ ph /\ ps)))
6		bnj984.3	. . . . 5 |- (ch <-> (n e. D /\ f Fn n /\ ph /\ ps))
7		bnj252 12091	. . . . 5 |- ((n e. D /\ f Fn n /\ ph /\ ps) <-> (n e. D /\ (f Fn n /\ ph /\ ps)))
8	6, 7	bitri 190	. . . 4 |- (ch <-> (n e. D /\ (f Fn n /\ ph /\ ps)))
9	5, 8	bnj133 12466	. . 3 |- (E.n e. D (f Fn n /\ ph /\ ps) <-> E.nch)
10	9	sbcbii 2506	. 2 |- (G e. A -> ([G / f]E.n e. D (f Fn n /\ ph /\ ps) <-> [G / f]E.nch))
11	4, 10	bitrd 587	1 |- (G e. A -> (G e. B <-> [G / f]E.nch))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  E.wex 1326  [wsbc 1534  {cab 1871  E.wrex 2106   Fn wfn 3993   /\ syn-bnj17 12019

This theorem is referenced by:  bnj985 13359

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-rex 2110  df-rab 2112  df-v 2294  df-sbc 2454  df-bnj17 12020

Copyright terms: Public domain