Description: Commutation of restricted and unrestricted existential quantifiers. (Contributed by NM, 12-Apr-2004) (Proof shortened by Andrew Salmon, 8-Jun-2011) Reduce axiom dependencies. (Revised by BJ, 13-Jun-2019)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | rexcom4 | ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 𝜑 ↔ ∃ 𝑦 ∃ 𝑥 ∈ 𝐴 𝜑 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | exdistr | ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 𝜑 ) ) | |
| 2 | df-rex | ⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) | |
| 3 | 2 | exbii | ⊢ ( ∃ 𝑦 ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑦 ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) |
| 4 | excom | ⊢ ( ∃ 𝑦 ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) | |
| 5 | 3 4 | bitri | ⊢ ( ∃ 𝑦 ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) |
| 6 | df-rex | ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 𝜑 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 𝜑 ) ) | |
| 7 | 1 5 6 | 3bitr4ri | ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 𝜑 ↔ ∃ 𝑦 ∃ 𝑥 ∈ 𝐴 𝜑 ) |