Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > axc11r | Structured version Visualization version GIF version |
Description: Same as axc11 2448 but with reversed antecedent. Note the use
of ax-12 2172
(and not merely ax12v 2173 as in axc11rv 2261).
This theorem is mostly used to eliminate conditions requiring set variables be distinct (cf. cbvaev 2054 and aecom 2445, 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 2386 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 2172 | . . 3 ⊢ (𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦(𝑦 = 𝑥 → 𝜑))) | |
2 | 1 | sps 2179 | . 2 ⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦(𝑦 = 𝑥 → 𝜑))) |
3 | pm2.27 42 | . . 3 ⊢ (𝑦 = 𝑥 → ((𝑦 = 𝑥 → 𝜑) → 𝜑)) | |
4 | 3 | al2imi 1812 | . 2 ⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑦(𝑦 = 𝑥 → 𝜑) → ∀𝑦𝜑)) |
5 | 2, 4 | syld 47 | 1 ⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1531 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-12 2172 |
This theorem depends on definitions: df-bi 209 df-ex 1777 |
This theorem is referenced by: ax12 2441 axc11n 2444 axc11 2448 hbae 2449 dral1 2457 dral1ALT 2458 sb4a 2505 axpowndlem3 10015 axc11n11r 34012 bj-ax12v3ALT 34015 bj-hbaeb2 34136 |
Copyright terms: Public domain | W3C validator |