Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > axc11r | Structured version Visualization version GIF version |
Description: Same as axc11 2429 but with reversed antecedent. Note the use
of ax-12 2177
(and not merely ax12v 2178 as in axc11rv 2264).
This theorem is mostly used to eliminate conditions requiring set variables be distinct (cf. cbvaev 2061 and aecom 2426, 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 2371 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 2184 | . 2 ⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦(𝑦 = 𝑥 → 𝜑))) |
3 | pm2.27 42 | . . 3 ⊢ (𝑦 = 𝑥 → ((𝑦 = 𝑥 → 𝜑) → 𝜑)) | |
4 | 3 | al2imi 1823 | . 2 ⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑦(𝑦 = 𝑥 → 𝜑) → ∀𝑦𝜑)) |
5 | 2, 4 | syld 47 | 1 ⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1541 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2018 ax-12 2177 |
This theorem depends on definitions: df-bi 210 df-ex 1788 |
This theorem is referenced by: ax12 2422 axc11n 2425 axc11 2429 hbae 2430 dral1 2438 dral1ALT 2439 sb4a 2483 axpowndlem3 10178 axc11n11r 34551 bj-ax12v3ALT 34554 bj-hbaeb2 34687 |
Copyright terms: Public domain | W3C validator |