| 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 2117. 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 disjoint variable 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 1910 | . . 3 ⊢ (𝑥 ∈ 𝑦 → ∀𝑧 𝑥 ∈ 𝑦) | |
| 2 | elequ1 2115 | . . 3 ⊢ (𝑧 = 𝑥 → (𝑧 ∈ 𝑦 ↔ 𝑥 ∈ 𝑦)) | |
| 3 | 1, 2 | equsexhv 2292 | . 2 ⊢ (∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝑦) ↔ 𝑥 ∈ 𝑦) |
| 4 | 3 | bicomi 224 | 1 ⊢ (𝑥 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝑦)) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∧ wa 395 ∃wex 1779 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-10 2141 ax-12 2177 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-nf 1784 |
| This theorem is referenced by: (None) |
| Copyright terms: Public domain | W3C validator |