This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - start with the Axiom of Extensionality Restricted quantification Restricted universal and existential quantification 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 ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ 𝐵 → 𝜑 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ 𝐴 → 𝜑 ) )