This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bnj106

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj106.1 
|- ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
bnj106.2 
|- F e. _V
Assertion bnj106 
|- ( [. F / f ]. [. 1o / n ]. ps <-> A. i e. _om ( suc i e. 1o -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) )

Proof

Step Hyp Ref Expression
1 bnj106.1 
 |-  ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
2 bnj106.2 
 |-  F e. _V
3 bnj105 
 |-  1o e. _V
4 1 3 bnj92 
 |-  ( [. 1o / n ]. ps <-> A. i e. _om ( suc i e. 1o -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
5 4 sbcbii 
 |-  ( [. F / f ]. [. 1o / n ]. ps <-> [. F / f ]. A. i e. _om ( suc i e. 1o -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
6 fveq1 
 |-  ( f = F -> ( f ` suc i ) = ( F ` suc i ) )
7 fveq1 
 |-  ( f = F -> ( f ` i ) = ( F ` i ) )
8 7 bnj1113 
 |-  ( f = F -> U_ y e. ( f ` i ) _pred ( y , A , R ) = U_ y e. ( F ` i ) _pred ( y , A , R ) )
9 6 8 eqeq12d 
 |-  ( f = F -> ( ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) <-> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) )
10 9 imbi2d 
 |-  ( f = F -> ( ( suc i e. 1o -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) <-> ( suc i e. 1o -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) ) )
11 10 ralbidv 
 |-  ( f = F -> ( A. i e. _om ( suc i e. 1o -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) <-> A. i e. _om ( suc i e. 1o -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) ) )
12 2 11 sbcie 
 |-  ( [. F / f ]. A. i e. _om ( suc i e. 1o -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) <-> A. i e. _om ( suc i e. 1o -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) )
13 5 12 bitri 
 |-  ( [. F / f ]. [. 1o / n ]. ps <-> A. i e. _om ( suc i e. 1o -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) )