Metamath Proof Explorer

Theorem r19.26m

Description: Version of 19.26 and r19.26 with restricted quantifiers ranging over different classes. (Contributed by NM, 22-Feb-2004)

Ref Expression
Assertion r19.26m ⊢ ∀ x x ∈ A → φ ∧ x ∈ B → ψ ↔ ∀ x ∈ A φ ∧ ∀ x ∈ B ψ

Proof

Step Hyp Ref Expression
1 19.26 ⊢ ∀ x x ∈ A → φ ∧ x ∈ B → ψ ↔ ∀ x x ∈ A → φ ∧ ∀ x x ∈ B → ψ
2 df-ral ⊢ ∀ x ∈ A φ ↔ ∀ x x ∈ A → φ
3 df-ral ⊢ ∀ x ∈ B ψ ↔ ∀ x x ∈ B → ψ
4 2 3 anbi12i ⊢ ∀ x ∈ A φ ∧ ∀ x ∈ B ψ ↔ ∀ x x ∈ A → φ ∧ ∀ x x ∈ B → ψ
5 1 4 bitr4i ⊢ ∀ x x ∈ A → φ ∧ x ∈ B → ψ ↔ ∀ x ∈ A φ ∧ ∀ x ∈ B ψ