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 | |- ( E. x e. A E. y ph <-> E. y E. x e. A ph ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | exdistr | |- ( E. x E. y ( x e. A /\ ph ) <-> E. x ( x e. A /\ E. y ph ) ) |
|
| 2 | df-rex | |- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) ) |
|
| 3 | 2 | exbii | |- ( E. y E. x e. A ph <-> E. y E. x ( x e. A /\ ph ) ) |
| 4 | excom | |- ( E. y E. x ( x e. A /\ ph ) <-> E. x E. y ( x e. A /\ ph ) ) |
|
| 5 | 3 4 | bitri | |- ( E. y E. x e. A ph <-> E. x E. y ( x e. A /\ ph ) ) |
| 6 | df-rex | |- ( E. x e. A E. y ph <-> E. x ( x e. A /\ E. y ph ) ) |
|
| 7 | 1 5 6 | 3bitr4ri | |- ( E. x e. A E. y ph <-> E. y E. x e. A ph ) |