Theorem ralsbii

Description: Congruence for "all some" restricted to a class. (Contributed by David A. Wheeler, 12-Jul-2026)

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

Proof

Step	Hyp	Ref	Expression
1		ralsbii.1	|- ( ph <-> ch )
2		ralsbii.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	rexbii	|- ( 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-rals	|- ( AE x e. A ( ph -> ps ) <-> ( A. x e. A ( ph -> ps ) /\ E. x e. A ph ) )
8		df-rals	|- ( 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 ) )