Metamath Proof Explorer

Theorem r19.26-2

Description: Restricted quantifier version of 19.26-2 . Version of r19.26 with two quantifiers. (Contributed by NM, 10-Aug-2004)

Ref Expression
Assertion r19.26-2 ⊢∀x∈A∀y∈Bφ∧ψ↔∀x∈A∀y∈Bφ∧∀x∈A∀y∈Bψ

Proof

Step Hyp Ref Expression
1 r19.26 ⊢∀y∈Bφ∧ψ↔∀y∈Bφ∧∀y∈Bψ
2 1 ralbii ⊢∀x∈A∀y∈Bφ∧ψ↔∀x∈A∀y∈Bφ∧∀y∈Bψ
3 r19.26 ⊢∀x∈A∀y∈Bφ∧∀y∈Bψ↔∀x∈A∀y∈Bφ∧∀x∈A∀y∈Bψ
4 2 3 bitri ⊢∀x∈A∀y∈Bφ∧ψ↔∀x∈A∀y∈Bφ∧∀x∈A∀y∈Bψ