Description: Duplication of wl-equsal1t , with shorter proof. If one imposes a disjoint variable condition on x,y , then one can use alequexv and reduce axiom dependencies, and similarly for the following theorems. Note: wl-equsalcom is also interesting. (Contributed by BJ, 6-Oct-2018)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-equsal1t | |- ( F/ x ph -> ( A. x ( x = y -> ph ) <-> ph ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bj-alequex | |- ( A. x ( x = y -> ph ) -> E. x ph ) |
|
| 2 | 19.9t | |- ( F/ x ph -> ( E. x ph <-> ph ) ) |
|
| 3 | 1 2 | syl5ib | |- ( F/ x ph -> ( A. x ( x = y -> ph ) -> ph ) ) |
| 4 | nf5r | |- ( F/ x ph -> ( ph -> A. x ph ) ) |
|
| 5 | ala1 | |- ( A. x ph -> A. x ( x = y -> ph ) ) |
|
| 6 | 4 5 | syl6 | |- ( F/ x ph -> ( ph -> A. x ( x = y -> ph ) ) ) |
| 7 | 3 6 | impbid | |- ( F/ x ph -> ( A. x ( x = y -> ph ) <-> ph ) ) |