Theorem iota4an

Description: Theorem *14.23 in WhiteheadRussell p. 191. (Contributed by Andrew Salmon, 12-Jul-2011)

	Ref	Expression
Assertion	iota4an	|- ( E! x ( ph /\ ps ) -> [. ( iota x ( ph /\ ps ) ) / x ]. ph )

Proof

Step	Hyp	Ref	Expression
1		iota4	|- ( E! x ( ph /\ ps ) -> [. ( iota x ( ph /\ ps ) ) / x ]. ( ph /\ ps ) )
2		iotaex	|- ( iota x ( ph /\ ps ) ) e. _V
3		simpl	|- ( ( ph /\ ps ) -> ph )
4	3	sbcth	|- ( ( iota x ( ph /\ ps ) ) e. _V -> [. ( iota x ( ph /\ ps ) ) / x ]. ( ( ph /\ ps ) -> ph ) )
5	2 4	ax-mp	|- [. ( iota x ( ph /\ ps ) ) / x ]. ( ( ph /\ ps ) -> ph )
6		sbcimg	|- ( ( iota x ( ph /\ ps ) ) e. _V -> ( [. ( iota x ( ph /\ ps ) ) / x ]. ( ( ph /\ ps ) -> ph ) <-> ( [. ( iota x ( ph /\ ps ) ) / x ]. ( ph /\ ps ) -> [. ( iota x ( ph /\ ps ) ) / x ]. ph ) ) )
7	2 6	ax-mp	|- ( [. ( iota x ( ph /\ ps ) ) / x ]. ( ( ph /\ ps ) -> ph ) <-> ( [. ( iota x ( ph /\ ps ) ) / x ]. ( ph /\ ps ) -> [. ( iota x ( ph /\ ps ) ) / x ]. ph ) )
8	5 7	mpbi	|- ( [. ( iota x ( ph /\ ps ) ) / x ]. ( ph /\ ps ) -> [. ( iota x ( ph /\ ps ) ) / x ]. ph )
9	1 8	syl	|- ( E! x ( ph /\ ps ) -> [. ( iota x ( ph /\ ps ) ) / x ]. ph )