Theorem alseubii

Description: Congruence: equivalents may be substituted inside an "all some one". This is the "all some one" counterpart of alsbii . (Contributed by David A. Wheeler, 21-Jul-2026)

	Ref	Expression
Hypotheses	alseubii.1	|- ( ph <-> ch )
	alseubii.2	|- ( ps <-> th )
Assertion	alseubii	|- ( AE! x ( ph -> ps ) <-> AE! x ( ch -> th ) )

Proof

Step	Hyp	Ref	Expression
1		alseubii.1	|- ( ph <-> ch )
2		alseubii.2	|- ( ps <-> th )
3	1 2	imbi12i	|- ( ( ph -> ps ) <-> ( ch -> th ) )
4	3	albii	|- ( A. x ( ph -> ps ) <-> A. x ( ch -> th ) )
5	1	eubii	|- ( E! x ph <-> E! x ch )
6	4 5	anbi12i	|- ( ( A. x ( ph -> ps ) /\ E! x ph ) <-> ( A. x ( ch -> th ) /\ E! x ch ) )
7		df-alseu	|- ( AE! x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E! x ph ) )
8		df-alseu	|- ( AE! x ( ch -> th ) <-> ( A. x ( ch -> th ) /\ E! x ch ) )
9	6 7 8	3bitr4i	|- ( AE! x ( ph -> ps ) <-> AE! x ( ch -> th ) )