Description: Same as axc11 but with reversed antecedent. Note the use of ax-12 (and not merely ax12v as in axc11rv ).
This theorem is mostly used to eliminate conditions requiring set variables be distinct (cf. cbvaev and aecom , for example) in proofs. In practice, theorems beyond elementary set theory do not really benefit from such eliminations. As of 2024, it is used in conjunction with ax-13 only, and like that, it should be applied only in niches where indispensable. (Contributed by NM, 25-Jul-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | axc11r | |- ( A. y y = x -> ( A. x ph -> A. y ph ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-12 | |- ( y = x -> ( A. x ph -> A. y ( y = x -> ph ) ) ) |
|
| 2 | 1 | sps | |- ( A. y y = x -> ( A. x ph -> A. y ( y = x -> ph ) ) ) |
| 3 | pm2.27 | |- ( y = x -> ( ( y = x -> ph ) -> ph ) ) |
|
| 4 | 3 | al2imi | |- ( A. y y = x -> ( A. y ( y = x -> ph ) -> A. y ph ) ) |
| 5 | 2 4 | syld | |- ( A. y y = x -> ( A. x ph -> A. y ph ) ) |