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

Metamath Proof Explorer

Theorem ralbii2

Description: Inference adding different restricted universal quantifiers to each side of an equivalence. (Contributed by NM, 15-Aug-2005)

Ref Expression
Hypothesis ralbii2.1 ⊢ x ∈ A → φ ↔ x ∈ B → ψ
Assertion ralbii2 ⊢ ∀ x ∈ A φ ↔ ∀ x ∈ B ψ

Proof

Step Hyp Ref Expression
1 ralbii2.1 ⊢ x ∈ A → φ ↔ x ∈ B → ψ
2 1 albii ⊢ ∀ x x ∈ A → φ ↔ ∀ x x ∈ B → ψ
3 df-ral ⊢ ∀ x ∈ A φ ↔ ∀ x x ∈ A → φ
4 df-ral ⊢ ∀ x ∈ B ψ ↔ ∀ x x ∈ B → ψ
5 2 3 4 3bitr4i ⊢ ∀ x ∈ A φ ↔ ∀ x ∈ B ψ