This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ralrmo3

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

Ref Expression
Assertion ralrmo3 ⊢ ∀ y ∈ B ∃* x ∈ A φ ↔ ∀ y ∃* x ∈ A y ∈ B ∧ φ

Proof

Step Hyp Ref Expression
1 df-ral ⊢ ∀ y ∈ B ∃* x ∈ A φ ↔ ∀ y y ∈ B → ∃* x ∈ A φ
2 nfv ⊢ Ⅎ x y ∈ B
3 2 rmoanim ⊢ ∃* x ∈ A y ∈ B ∧ φ ↔ y ∈ B → ∃* x ∈ A φ
4 3 albii ⊢ ∀ y ∃* x ∈ A y ∈ B ∧ φ ↔ ∀ y y ∈ B → ∃* x ∈ A φ
5 1 4 bitr4i ⊢ ∀ y ∈ B ∃* x ∈ A φ ↔ ∀ y ∃* x ∈ A y ∈ B ∧ φ