![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > axc11r | Structured version Visualization version GIF version |
Description: Same as axc11 2432 but with reversed antecedent. Note the use
of ax-12 2174
(and not merely ax12v 2175 as in axc11rv 2262).
This theorem is mostly used to eliminate conditions requiring set variables be distinct (cf. cbvaev 2050 and aecom 2429, 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 2374 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 2174 | . . 3 ⊢ (𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦(𝑦 = 𝑥 → 𝜑))) | |
2 | 1 | sps 2182 | . 2 ⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦(𝑦 = 𝑥 → 𝜑))) |
3 | pm2.27 42 | . . 3 ⊢ (𝑦 = 𝑥 → ((𝑦 = 𝑥 → 𝜑) → 𝜑)) | |
4 | 3 | al2imi 1811 | . 2 ⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑦(𝑦 = 𝑥 → 𝜑) → ∀𝑦𝜑)) |
5 | 2, 4 | syld 47 | 1 ⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1534 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-12 2174 |
This theorem depends on definitions: df-bi 207 df-ex 1776 |
This theorem is referenced by: ax12 2425 axc11n 2428 axc11 2432 hbae 2433 dral1 2441 dral1ALT 2442 sb4a 2482 axpowndlem3 10636 axc11n11r 36665 bj-ax12v3ALT 36668 bj-hbaeb2 36800 |
Copyright terms: Public domain | W3C validator |