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 ) )