![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > axc11r | Structured version Visualization version GIF version |
Description: Same as axc11 2428 but with reversed antecedent. Note the use
of ax-12 2170
(and not merely ax12v 2171 as in axc11rv 2255).
This theorem is mostly used to eliminate conditions requiring set variables be distinct (cf. cbvaev 2055 and aecom 2425, 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 2370 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 2170 | . . 3 ⊢ (𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦(𝑦 = 𝑥 → 𝜑))) | |
2 | 1 | sps 2177 | . 2 ⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦(𝑦 = 𝑥 → 𝜑))) |
3 | pm2.27 42 | . . 3 ⊢ (𝑦 = 𝑥 → ((𝑦 = 𝑥 → 𝜑) → 𝜑)) | |
4 | 3 | al2imi 1816 | . 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 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-12 2170 |
This theorem depends on definitions: df-bi 206 df-ex 1781 |
This theorem is referenced by: ax12 2421 axc11n 2424 axc11 2428 hbae 2429 dral1 2437 dral1ALT 2438 sb4a 2478 axpowndlem3 10600 axc11n11r 36025 bj-ax12v3ALT 36028 bj-hbaeb2 36160 |
Copyright terms: Public domain | W3C validator |