Metamath Proof Explorer

Theorem sbaniota

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

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

Step	Hyp	Ref	Expression
1		eupickbi	\|- ( E! x ph -> ( E. x ( ph /\ ps ) <-> A. x ( ph -> ps ) ) )
2		sbiota1	\|- ( E! x ph -> ( A. x ( ph -> ps ) <-> [. ( iota x ph ) / x ]. ps ) )
3	1 2	bitrd	\|- ( E! x ph -> ( E. x ( ph /\ ps ) <-> [. ( iota x ph ) / x ]. ps ) )

Step

Hyp

Ref

Expression

 |-  ( E! x ph -> ( E. x ( ph /\ ps ) <-> A. x ( ph -> ps ) ) )

 |-  ( E! x ph -> ( A. x ( ph -> ps ) <-> [. ( iota x ph ) / x ]. ps ) )

1 2

 |-  ( E! x ph -> ( E. x ( ph /\ ps ) <-> [. ( iota x ph ) / x ]. ps ) )