![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cleljustALT | Structured version Visualization version GIF version |
Description: Alternate proof of cleljust 2153. It is kept here and should not be modified because it is referenced on the Metamath Proof Explorer Home Page (mmset.html) as an example of how DV conditions are inherited by substitutions. (Contributed by NM, 28-Jan-2004.) (Revised by BJ, 29-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
cleljustALT | ⊢ (𝑥 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝑦)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-5 1991 | . . 3 ⊢ (𝑥 ∈ 𝑦 → ∀𝑧 𝑥 ∈ 𝑦) | |
2 | elequ1 2152 | . . 3 ⊢ (𝑧 = 𝑥 → (𝑧 ∈ 𝑦 ↔ 𝑥 ∈ 𝑦)) | |
3 | 1, 2 | equsexhv 2288 | . 2 ⊢ (∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝑦) ↔ 𝑥 ∈ 𝑦) |
4 | 3 | bicomi 214 | 1 ⊢ (𝑥 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝑦)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∧ wa 382 ∃wex 1852 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-8 2147 ax-10 2174 ax-12 2203 |
This theorem depends on definitions: df-bi 197 df-an 383 df-ex 1853 df-nf 1858 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |