Theorem ralseubii

Description: Congruence for "all some one" restricted to a class. This is the "all some one" counterpart of ralsbii . (Contributed by David A. Wheeler, 21-Jul-2026)

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

Proof

Step	Hyp	Ref	Expression
1		ralseubii.1	|- ( ph <-> ch )
2		ralseubii.2	|- ( ps <-> th )
3	1 2	imbi12i	|- ( ( ph -> ps ) <-> ( ch -> th ) )
4	3	ralbii	|- ( A. x e. A ( ph -> ps ) <-> A. x e. A ( ch -> th ) )
5	1	reubii	|- ( E! x e. A ph <-> E! x e. A ch )
6	4 5	anbi12i	|- ( ( A. x e. A ( ph -> ps ) /\ E! x e. A ph ) <-> ( A. x e. A ( ch -> th ) /\ E! x e. A ch ) )
7		df-ralseu	|- ( AE! x e. A ( ph -> ps ) <-> ( A. x e. A ( ph -> ps ) /\ E! x e. A ph ) )
8		df-ralseu	|- ( AE! x e. A ( ch -> th ) <-> ( A. x e. A ( ch -> th ) /\ E! x e. A ch ) )
9	6 7 8	3bitr4i	|- ( AE! x e. A ( ph -> ps ) <-> AE! x e. A ( ch -> th ) )