Description: Commutation of restricted and unrestricted universal quantifiers. (Contributed by NM, 26-Mar-2004) (Proof shortened by Andrew Salmon, 8-Jun-2011) Reduce axiom dependencies. (Revised by BJ, 13-Jun-2019) (Proof shortened by Wolf Lammen, 31-Oct-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ralcom4 | ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 𝜑 ↔ ∀ 𝑦 ∀ 𝑥 ∈ 𝐴 𝜑 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 19.21v | ⊢ ( ∀ 𝑦 ( 𝑥 ∈ 𝐴 → 𝜑 ) ↔ ( 𝑥 ∈ 𝐴 → ∀ 𝑦 𝜑 ) ) | |
| 2 | 1 | albii | ⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 ∈ 𝐴 → 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑦 𝜑 ) ) |
| 3 | alcom | ⊢ ( ∀ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 ∈ 𝐴 → 𝜑 ) ) | |
| 4 | df-ral | ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑦 𝜑 ) ) | |
| 5 | 2 3 4 | 3bitr4ri | ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 𝜑 ↔ ∀ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ) |
| 6 | df-ral | ⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ) | |
| 7 | 6 | albii | ⊢ ( ∀ 𝑦 ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ) |
| 8 | 5 7 | bitr4i | ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 𝜑 ↔ ∀ 𝑦 ∀ 𝑥 ∈ 𝐴 𝜑 ) |