Theorem ralbidb

Description: Formula-building rule for restricted universal quantifier and additional condition (deduction form). See ralbidc for a more generalized form. (Contributed by Zhi Wang, 6-Sep-2024)

	Ref	Expression
Hypotheses	ralbidb.1	|- ( ph -> ( x e. A <-> ( x e. B /\ ps ) ) )
	ralbidb.2	|- ( ( ph /\ x e. A ) -> ( ch <-> th ) )
Assertion	ralbidb	|- ( ph -> ( A. x e. A ch <-> A. x e. B ( ps -> th ) ) )

Proof

Step	Hyp	Ref	Expression
1		ralbidb.1	|- ( ph -> ( x e. A <-> ( x e. B /\ ps ) ) )
2		ralbidb.2	|- ( ( ph /\ x e. A ) -> ( ch <-> th ) )
3	1 2	logic1a	|- ( ph -> ( ( x e. A -> ch ) <-> ( ( x e. B /\ ps ) -> th ) ) )
4		impexp	|- ( ( ( x e. B /\ ps ) -> th ) <-> ( x e. B -> ( ps -> th ) ) )
5	3 4	bitrdi	|- ( ph -> ( ( x e. A -> ch ) <-> ( x e. B -> ( ps -> th ) ) ) )
6	5	ralbidv2	|- ( ph -> ( A. x e. A ch <-> A. x e. B ( ps -> th ) ) )