Theorem ralrmo3

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

	Ref	Expression
Assertion	ralrmo3	⊢ ( ∀ 𝑦 ∈ 𝐵 ∃* 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		df-ral	⊢ ( ∀ 𝑦 ∈ 𝐵 ∃* 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐵 → ∃* 𝑥 ∈ 𝐴 𝜑 ) )
2		nfv	⊢ Ⅎ 𝑥 𝑦 ∈ 𝐵
3	2	rmoanim	⊢ ( ∃* 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ↔ ( 𝑦 ∈ 𝐵 → ∃* 𝑥 ∈ 𝐴 𝜑 ) )
4	3	albii	⊢ ( ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐵 → ∃* 𝑥 ∈ 𝐴 𝜑 ) )
5	1 4	bitr4i	⊢ ( ∀ 𝑦 ∈ 𝐵 ∃* 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) )