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	$$⊢\phi \to \left(x\in A\leftrightarrow \left(x\in B\wedge \psi \right)\right)$$
	ralbidb.2	$$⊢\left(\phi \wedge x\in A\right)\to \left(\chi \leftrightarrow \theta \right)$$
Assertion	ralbidb	$$⊢\phi \to \left(\forall x\in A\chi \leftrightarrow \forall x\in B\left(\psi \to \theta \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ralbidb.1	$$⊢\phi \to \left(x\in A\leftrightarrow \left(x\in B\wedge \psi \right)\right)$$
2		ralbidb.2	$$⊢\left(\phi \wedge x\in A\right)\to \left(\chi \leftrightarrow \theta \right)$$
3	1 2	imbi12d2a	$$⊢\phi \to \left(\left(x\in A\to \chi \right)\leftrightarrow \left(\left(x\in B\wedge \psi \right)\to \theta \right)\right)$$
4		impexp	$$⊢\left(\left(x\in B\wedge \psi \right)\to \theta \right)\leftrightarrow \left(x\in B\to \left(\psi \to \theta \right)\right)$$
5	3 4	bitrdi	$$⊢\phi \to \left(\left(x\in A\to \chi \right)\leftrightarrow \left(x\in B\to \left(\psi \to \theta \right)\right)\right)$$
6	5	ralbidv2	$$⊢\phi \to \left(\forall x\in A\chi \leftrightarrow \forall x\in B\left(\psi \to \theta \right)\right)$$