Metamath Proof Explorer


Theorem ralcom3

Description: A commutation law for restricted universal quantifiers that swaps the domains of the restriction. (Contributed by NM, 22-Feb-2004) (Proof shortened by Wolf Lammen, 22-Dec-2024)

Ref Expression
Assertion ralcom3 ( ∀ 𝑥𝐴 ( 𝑥𝐵𝜑 ) ↔ ∀ 𝑥𝐵 ( 𝑥𝐴𝜑 ) )

Proof

Step Hyp Ref Expression
1 bi2.04 ( ( 𝑥𝐴 → ( 𝑥𝐵𝜑 ) ) ↔ ( 𝑥𝐵 → ( 𝑥𝐴𝜑 ) ) )
2 1 ralbii2 ( ∀ 𝑥𝐴 ( 𝑥𝐵𝜑 ) ↔ ∀ 𝑥𝐵 ( 𝑥𝐴𝜑 ) )