Theorem ralrmo3

Description: Pull a restricted universal quantifier into the body (for E* ). (Contributed by Peter Mazsa, 9-May-2019)

	Ref	Expression
Assertion	ralrmo3	$$⊢\forall y\in B{\exists }^{*}x\in A\phi \leftrightarrow \forall y{\exists }^{*}x\in A\left(y\in B\wedge \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		df-ral	$$⊢\forall y\in B{\exists }^{*}x\in A\phi \leftrightarrow \forall y\left(y\in B\to {\exists }^{*}x\in A\phi \right)$$
2		nfv	$$⊢Ⅎxy\in B$$
3	2	rmoanim	$$⊢{\exists }^{*}x\in A\left(y\in B\wedge \phi \right)\leftrightarrow \left(y\in B\to {\exists }^{*}x\in A\phi \right)$$
4	3	albii	$$⊢\forall y{\exists }^{*}x\in A\left(y\in B\wedge \phi \right)\leftrightarrow \forall y\left(y\in B\to {\exists }^{*}x\in A\phi \right)$$
5	1 4	bitr4i	$$⊢\forall y\in B{\exists }^{*}x\in A\phi \leftrightarrow \forall y{\exists }^{*}x\in A\left(y\in B\wedge \phi \right)$$