| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > axc11r | Structured version Visualization version GIF version | ||
| Description: Same as axc11 2435 but with reversed antecedent. Note the use
of ax-12 2177
(and not merely ax12v 2178 as in axc11rv 2265).
This theorem is mostly used to eliminate conditions requiring set variables be distinct (cf. cbvaev 2053 and aecom 2432, 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 2377 only, and like that, it should be applied only in niches where indispensable. (Contributed by NM, 25-Jul-2015.) |
| Ref | Expression |
|---|---|
| axc11r | ⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦𝜑)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-12 2177 | . . 3 ⊢ (𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦(𝑦 = 𝑥 → 𝜑))) | |
| 2 | 1 | sps 2185 | . 2 ⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦(𝑦 = 𝑥 → 𝜑))) |
| 3 | pm2.27 42 | . . 3 ⊢ (𝑦 = 𝑥 → ((𝑦 = 𝑥 → 𝜑) → 𝜑)) | |
| 4 | 3 | al2imi 1815 | . 2 ⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑦(𝑦 = 𝑥 → 𝜑) → ∀𝑦𝜑)) |
| 5 | 2, 4 | syld 47 | 1 ⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦𝜑)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∀wal 1538 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-12 2177 |
| This theorem depends on definitions: df-bi 207 df-ex 1780 |
| This theorem is referenced by: ax12 2428 axc11n 2431 axc11 2435 hbae 2436 dral1 2444 dral1ALT 2445 sb4a 2485 axpowndlem3 10639 axc11n11r 36684 bj-ax12v3ALT 36687 bj-hbaeb2 36819 |
| Copyright terms: Public domain | W3C validator |