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 ( ∀ 𝑥𝐴𝑦𝐵 ( 𝜑𝜓 ) ↔ ( ∀ 𝑥𝐴𝑦𝐵 𝜑 ∧ ∀ 𝑥𝐴𝑦𝐵 𝜓 ) )

Proof

Step Hyp Ref Expression
1 r19.26 ( ∀ 𝑦𝐵 ( 𝜑𝜓 ) ↔ ( ∀ 𝑦𝐵 𝜑 ∧ ∀ 𝑦𝐵 𝜓 ) )
2 1 ralbii ( ∀ 𝑥𝐴𝑦𝐵 ( 𝜑𝜓 ) ↔ ∀ 𝑥𝐴 ( ∀ 𝑦𝐵 𝜑 ∧ ∀ 𝑦𝐵 𝜓 ) )
3 r19.26 ( ∀ 𝑥𝐴 ( ∀ 𝑦𝐵 𝜑 ∧ ∀ 𝑦𝐵 𝜓 ) ↔ ( ∀ 𝑥𝐴𝑦𝐵 𝜑 ∧ ∀ 𝑥𝐴𝑦𝐵 𝜓 ) )
4 2 3 bitri ( ∀ 𝑥𝐴𝑦𝐵 ( 𝜑𝜓 ) ↔ ( ∀ 𝑥𝐴𝑦𝐵 𝜑 ∧ ∀ 𝑥𝐴𝑦𝐵 𝜓 ) )