Theorem bnj1040 31040

Description: Technical lemma for bnj69 31078. 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.)

Hypotheses

Ref	Expression
bnj1040.1	|- ( ph' <-> [. j / i ]. ph )
bnj1040.2	|- ( ps' <-> [. j / i ]. ps )
bnj1040.3	|- ( ch <-> ( n e. D /\ f Fn n /\ ph /\ ps ) )
bnj1040.4	|- ( ch' <-> [. j / i ]. ch )

Assertion

Ref	Expression
bnj1040	|- ( ch' <-> ( n e. D /\ f Fn n /\ ph' /\ ps' ) )

Distinct variable groups:   D, i   f, i   i, n

Allowed substitution hints:   ph( f, i, j, n)   ps( f, i, j, n)   ch( f, i, j, n)   D( f, j, n)   ph'( f, i, j, n)   ps'( f, i, j, n)   ch'( f, i, j, n)

Proof of Theorem bnj1040

Step	Hyp	Ref	Expression
1		bnj1040.4	. 2 |- ( ch' <-> [. j / i ]. ch )
2		bnj1040.3	. . 3 |- ( ch <-> ( n e. D /\ f Fn n /\ ph /\ ps ) )
3	2	sbcbii 3491	. 2 |- ( [. j / i ]. ch <-> [. j / i ]. ( n e. D /\ f Fn n /\ ph /\ ps ) )
4		df-bnj17 30753	. . 3 |- ( ( [. j / i ]. n e. D /\ [. j / i ]. f Fn n /\ [. j / i ]. ph /\ [. j / i ]. ps ) <-> ( ( [. j / i ]. n e. D /\ [. j / i ]. f Fn n /\ [. j / i ]. ph ) /\ [. j / i ]. ps ) )
5		vex 3203	. . . . . 6 |- j e. _V
6	5	bnj525 30807	. . . . 5 |- ( [. j / i ]. n e. D <-> n e. D )
7	6	bicomi 214	. . . 4 |- ( n e. D <-> [. j / i ]. n e. D )
8	5	bnj525 30807	. . . . 5 |- ( [. j / i ]. f Fn n <-> f Fn n )
9	8	bicomi 214	. . . 4 |- ( f Fn n <-> [. j / i ]. f Fn n )
10		bnj1040.1	. . . 4 |- ( ph' <-> [. j / i ]. ph )
11		bnj1040.2	. . . 4 |- ( ps' <-> [. j / i ]. ps )
12	7, 9, 10, 11	bnj887 30835	. . 3 |- ( ( n e. D /\ f Fn n /\ ph' /\ ps' ) <-> ( [. j / i ]. n e. D /\ [. j / i ]. f Fn n /\ [. j / i ]. ph /\ [. j / i ]. ps ) )
13		df-bnj17 30753	. . . . 5 |- ( ( n e. D /\ f Fn n /\ ph /\ ps ) <-> ( ( n e. D /\ f Fn n /\ ph ) /\ ps ) )
14	13	sbcbii 3491	. . . 4 |- ( [. j / i ]. ( n e. D /\ f Fn n /\ ph /\ ps ) <-> [. j / i ]. ( ( n e. D /\ f Fn n /\ ph ) /\ ps ) )
15		sbcan 3478	. . . 4 |- ( [. j / i ]. ( ( n e. D /\ f Fn n /\ ph ) /\ ps ) <-> ( [. j / i ]. ( n e. D /\ f Fn n /\ ph ) /\ [. j / i ]. ps ) )
16		sbc3an 3494	. . . . 5 |- ( [. j / i ]. ( n e. D /\ f Fn n /\ ph ) <-> ( [. j / i ]. n e. D /\ [. j / i ]. f Fn n /\ [. j / i ]. ph ) )
17	16	anbi1i 731	. . . 4 |- ( ( [. j / i ]. ( n e. D /\ f Fn n /\ ph ) /\ [. j / i ]. ps ) <-> ( ( [. j / i ]. n e. D /\ [. j / i ]. f Fn n /\ [. j / i ]. ph ) /\ [. j / i ]. ps ) )
18	14, 15, 17	3bitri 286	. . 3 |- ( [. j / i ]. ( n e. D /\ f Fn n /\ ph /\ ps ) <-> ( ( [. j / i ]. n e. D /\ [. j / i ]. f Fn n /\ [. j / i ]. ph ) /\ [. j / i ]. ps ) )
19	4, 12, 18	3bitr4ri 293	. 2 |- ( [. j / i ]. ( n e. D /\ f Fn n /\ ph /\ ps ) <-> ( n e. D /\ f Fn n /\ ph' /\ ps' ) )
20	1, 3, 19	3bitri 286	1 |- ( ch' <-> ( n e. D /\ f Fn n /\ ph' /\ ps' ) )

Syntax hints:   <-> wb 196   /\ wa 384   /\ w3a 1037   e. wcel 1990   [.wsbc 3435   Fn wfn 5883   /\ w-bnj17 30752

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-v 3202  df-sbc 3436  df-bnj17 30753

This theorem is referenced by:  bnj1128  31058