![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cleljust | Structured version Visualization version GIF version |
Description: When the class variables in definition df-clel 2774 are replaced with setvar variables, this theorem of predicate calculus is the result. This theorem provides part of the justification for the consistency of that definition, which "overloads" the setvar variables in wel 2108 with the class variables in wcel 2107. (Contributed by NM, 28-Jan-2004.) Revised to use equsexvw 2052 in order to remove dependencies on ax-10 2135, ax-12 2163, ax-13 2334. Note that there is no disjoint variable condition on 𝑥, 𝑦, that is, on the variables of the left-hand side, as should be the case for definitions. (Revised by BJ, 29-Dec-2020.) |
Ref | Expression |
---|---|
cleljust | ⊢ (𝑥 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝑦)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elequ1 2114 | . . 3 ⊢ (𝑧 = 𝑥 → (𝑧 ∈ 𝑦 ↔ 𝑥 ∈ 𝑦)) | |
2 | 1 | equsexvw 2052 | . 2 ⊢ (∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝑦) ↔ 𝑥 ∈ 𝑦) |
3 | 2 | bicomi 216 | 1 ⊢ (𝑥 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝑦)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 ∧ wa 386 ∃wex 1823 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-8 2109 |
This theorem depends on definitions: df-bi 199 df-an 387 df-ex 1824 |
This theorem is referenced by: bj-dfclel 33460 |
Copyright terms: Public domain | W3C validator |