Theorem 2ralbida

Description: Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 24-Feb-2004)

	Ref	Expression
Hypotheses	2ralbida.1	$$⊢Ⅎx\phi$$
	2ralbida.2	$$⊢Ⅎy\phi$$
	2ralbida.3	$$⊢\left(\phi \wedge \left(x\in A\wedge y\in B\right)\right)\to \left(\psi \leftrightarrow \chi \right)$$
Assertion	2ralbida	$$⊢\phi \to \left(\forall x\in A\forall y\in B\psi \leftrightarrow \forall x\in A\forall y\in B\chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		2ralbida.1	$$⊢Ⅎx\phi$$
2		2ralbida.2	$$⊢Ⅎy\phi$$
3		2ralbida.3	$$⊢\left(\phi \wedge \left(x\in A\wedge y\in B\right)\right)\to \left(\psi \leftrightarrow \chi \right)$$
4		nfv	$$⊢Ⅎyx\in A$$
5	2 4	nfan	$$⊢Ⅎy\left(\phi \wedge x\in A\right)$$
6	3	anassrs	$$⊢\left(\left(\phi \wedge x\in A\right)\wedge y\in B\right)\to \left(\psi \leftrightarrow \chi \right)$$
7	5 6	ralbida	$$⊢\left(\phi \wedge x\in A\right)\to \left(\forall y\in B\psi \leftrightarrow \forall y\in B\chi \right)$$
8	1 7	ralbida	$$⊢\phi \to \left(\forall x\in A\forall y\in B\psi \leftrightarrow \forall x\in A\forall y\in B\chi \right)$$