Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ax9v | Structured version Visualization version GIF version |
Description: Weakened version of ax-9 2122, with a disjoint variable condition on 𝑥, 𝑦. This should be the only proof referencing ax-9 2122, and it should be referenced only by its two weakened versions ax9v1 2124 and ax9v2 2125, from which ax-9 2122 is then rederived as ax9 2126, which shows that either ax9v 2123 or the conjunction of ax9v1 2124 and ax9v2 2125 is sufficient. (Contributed by BJ, 7-Dec-2020.) Use ax9 2126 instead. (New usage is discouraged.) |
Ref | Expression |
---|---|
ax9v | ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-9 2122 | 1 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 |
This theorem was proved from axioms: ax-9 2122 |
This theorem is referenced by: ax9v1 2124 ax9v2 2125 |
Copyright terms: Public domain | W3C validator |