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

Metamath Proof Explorer

Theorem bnj156

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

Ref Expression
Hypotheses bnj156.1 
|- ( ze0 <-> ( f Fn 1o /\ ph' /\ ps' ) )
bnj156.2 
|- ( ze1 <-> [. g / f ]. ze0 )
bnj156.3 
|- ( ph1 <-> [. g / f ]. ph' )
bnj156.4 
|- ( ps1 <-> [. g / f ]. ps' )
Assertion bnj156 
|- ( ze1 <-> ( g Fn 1o /\ ph1 /\ ps1 ) )

Proof

Step Hyp Ref Expression
1 bnj156.1 
 |-  ( ze0 <-> ( f Fn 1o /\ ph' /\ ps' ) )
2 bnj156.2 
 |-  ( ze1 <-> [. g / f ]. ze0 )
3 bnj156.3 
 |-  ( ph1 <-> [. g / f ]. ph' )
4 bnj156.4 
 |-  ( ps1 <-> [. g / f ]. ps' )
5 1 sbcbii 
 |-  ( [. g / f ]. ze0 <-> [. g / f ]. ( f Fn 1o /\ ph' /\ ps' ) )
6 sbc3an 
 |-  ( [. g / f ]. ( f Fn 1o /\ ph' /\ ps' ) <-> ( [. g / f ]. f Fn 1o /\ [. g / f ]. ph' /\ [. g / f ]. ps' ) )
7 bnj62 
 |-  ( [. g / f ]. f Fn 1o <-> g Fn 1o )
8 3 bicomi 
 |-  ( [. g / f ]. ph' <-> ph1 )
9 4 bicomi 
 |-  ( [. g / f ]. ps' <-> ps1 )
10 7 8 9 3anbi123i 
 |-  ( ( [. g / f ]. f Fn 1o /\ [. g / f ]. ph' /\ [. g / f ]. ps' ) <-> ( g Fn 1o /\ ph1 /\ ps1 ) )
11 6 10 bitri 
 |-  ( [. g / f ]. ( f Fn 1o /\ ph' /\ ps' ) <-> ( g Fn 1o /\ ph1 /\ ps1 ) )
12 5 11 bitri 
 |-  ( [. g / f ]. ze0 <-> ( g Fn 1o /\ ph1 /\ ps1 ) )
13 2 12 bitri 
 |-  ( ze1 <-> ( g Fn 1o /\ ph1 /\ ps1 ) )