Theorem bnj523 29746

Description: Technical lemma for bnj852 29780. 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
bnj523.1	|- ( ph <-> ( F ` (/) ) = pred ( X , A , R ) )
bnj523.2	|- ( ph' <-> [. M / n ]. ph )
bnj523.3	|- M e. _V

Assertion

Ref	Expression
bnj523	|- ( ph' <-> ( F ` (/) ) = pred ( X , A , R ) )

Distinct variable groups:   A, n   n, F   R, n   n, X

Allowed substitution hints:   ph( n)   M( n)   ph'( n)

Proof of Theorem bnj523

Step	Hyp	Ref	Expression
1		bnj523.2	. 2 |- ( ph' <-> [. M / n ]. ph )
2		bnj523.1	. . 3 |- ( ph <-> ( F ` (/) ) = pred ( X , A , R ) )
3	2	sbcbii 3334	. 2 |- ( [. M / n ]. ph <-> [. M / n ]. ( F ` (/) ) = pred ( X , A , R ) )
4		bnj523.3	. . 3 |- M e. _V
5	4	bnj525 29595	. 2 |- ( [. M / n ]. ( F ` (/) ) = pred ( X , A , R ) <-> ( F ` (/) ) = pred ( X , A , R ) )
6	1, 3, 5	3bitri 279	1 |- ( ph' <-> ( F ` (/) ) = pred ( X , A , R ) )

Syntax hints:   <-> wb 189   = wceq 1454   e. wcel 1897   _Vcvv 3056   [.wsbc 3278   (/)c0 3742   ` cfv 5600   predc-bnj14 29541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-v 3058  df-sbc 3279

This theorem is referenced by:  bnj600  29778  bnj908  29790  bnj934  29794