Metamath Proof Explorer


Theorem bnj121

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

Ref Expression
Hypotheses bnj121.1
|- ( ze <-> ( ( R _FrSe A /\ x e. A ) -> ( f Fn n /\ ph /\ ps ) ) )
bnj121.2
|- ( ze' <-> [. 1o / n ]. ze )
bnj121.3
|- ( ph' <-> [. 1o / n ]. ph )
bnj121.4
|- ( ps' <-> [. 1o / n ]. ps )
Assertion bnj121
|- ( ze' <-> ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) )

Proof

Step Hyp Ref Expression
1 bnj121.1
 |-  ( ze <-> ( ( R _FrSe A /\ x e. A ) -> ( f Fn n /\ ph /\ ps ) ) )
2 bnj121.2
 |-  ( ze' <-> [. 1o / n ]. ze )
3 bnj121.3
 |-  ( ph' <-> [. 1o / n ]. ph )
4 bnj121.4
 |-  ( ps' <-> [. 1o / n ]. ps )
5 1 sbcbii
 |-  ( [. 1o / n ]. ze <-> [. 1o / n ]. ( ( R _FrSe A /\ x e. A ) -> ( f Fn n /\ ph /\ ps ) ) )
6 bnj105
 |-  1o e. _V
7 6 bnj90
 |-  ( [. 1o / n ]. f Fn n <-> f Fn 1o )
8 7 bicomi
 |-  ( f Fn 1o <-> [. 1o / n ]. f Fn n )
9 8 3 4 3anbi123i
 |-  ( ( f Fn 1o /\ ph' /\ ps' ) <-> ( [. 1o / n ]. f Fn n /\ [. 1o / n ]. ph /\ [. 1o / n ]. ps ) )
10 sbc3an
 |-  ( [. 1o / n ]. ( f Fn n /\ ph /\ ps ) <-> ( [. 1o / n ]. f Fn n /\ [. 1o / n ]. ph /\ [. 1o / n ]. ps ) )
11 9 10 bitr4i
 |-  ( ( f Fn 1o /\ ph' /\ ps' ) <-> [. 1o / n ]. ( f Fn n /\ ph /\ ps ) )
12 11 imbi2i
 |-  ( ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) <-> ( ( R _FrSe A /\ x e. A ) -> [. 1o / n ]. ( f Fn n /\ ph /\ ps ) ) )
13 nfv
 |-  F/ n ( R _FrSe A /\ x e. A )
14 13 sbc19.21g
 |-  ( 1o e. _V -> ( [. 1o / n ]. ( ( R _FrSe A /\ x e. A ) -> ( f Fn n /\ ph /\ ps ) ) <-> ( ( R _FrSe A /\ x e. A ) -> [. 1o / n ]. ( f Fn n /\ ph /\ ps ) ) ) )
15 6 14 ax-mp
 |-  ( [. 1o / n ]. ( ( R _FrSe A /\ x e. A ) -> ( f Fn n /\ ph /\ ps ) ) <-> ( ( R _FrSe A /\ x e. A ) -> [. 1o / n ]. ( f Fn n /\ ph /\ ps ) ) )
16 12 15 bitr4i
 |-  ( ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) <-> [. 1o / n ]. ( ( R _FrSe A /\ x e. A ) -> ( f Fn n /\ ph /\ ps ) ) )
17 5 2 16 3bitr4i
 |-  ( ze' <-> ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) )