Description: Double quantification with "at most one". Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker 2moexv when possible. (Contributed by NM, 3-Dec-2001) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | 2moex | |- ( E* x E. y ph -> A. y E* x ph ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfe1 | |- F/ y E. y ph |
|
| 2 | 1 | nfmo | |- F/ y E* x E. y ph |
| 3 | 19.8a | |- ( ph -> E. y ph ) |
|
| 4 | 3 | moimi | |- ( E* x E. y ph -> E* x ph ) |
| 5 | 2 4 | alrimi | |- ( E* x E. y ph -> A. y E* x ph ) |