Metamath Proof Explorer

Theorem 4ralbii

Description: Inference adding four restricted universal quantifiers to both sides of an equivalence. (Contributed by Scott Fenton, 28-Feb-2025)

Ref Expression
Hypothesis 4ralbii.1 ⊢ φ ↔ ψ
Assertion 4ralbii ⊢ ∀ x ∈ A ∀ y ∈ B ∀ z ∈ C ∀ w ∈ D φ ↔ ∀ x ∈ A ∀ y ∈ B ∀ z ∈ C ∀ w ∈ D ψ

Proof

Step Hyp Ref Expression
1 4ralbii.1 ⊢ φ ↔ ψ
2 1 ralbii ⊢ ∀ w ∈ D φ ↔ ∀ w ∈ D ψ
3 2 3ralbii ⊢ ∀ x ∈ A ∀ y ∈ B ∀ z ∈ C ∀ w ∈ D φ ↔ ∀ x ∈ A ∀ y ∈ B ∀ z ∈ C ∀ w ∈ D ψ