![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > equsexALT | Structured version Visualization version GIF version |
Description: Alternate proof of equsex 2415. This proves the result directly, instead of as a corollary of equsal 2414 via equs4 2413. Note in particular that only existential quantifiers appear in the proof and that the only step requiring ax-13 2369 is ax6e 2380. This proof mimics that of equsal 2414 (in particular, note that pm5.32i 573, exbii 1848, 19.41 2226, mpbiran 705 correspond respectively to pm5.74i 270, albii 1819, 19.23 2202, a1bi 361). (Contributed by BJ, 20-Aug-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
equsal.1 | ⊢ Ⅎ𝑥𝜓 |
equsal.2 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
equsexALT | ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | equsal.2 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
2 | 1 | pm5.32i 573 | . . 3 ⊢ ((𝑥 = 𝑦 ∧ 𝜑) ↔ (𝑥 = 𝑦 ∧ 𝜓)) |
3 | 2 | exbii 1848 | . 2 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜓)) |
4 | ax6e 2380 | . . 3 ⊢ ∃𝑥 𝑥 = 𝑦 | |
5 | equsal.1 | . . . 4 ⊢ Ⅎ𝑥𝜓 | |
6 | 5 | 19.41 2226 | . . 3 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜓) ↔ (∃𝑥 𝑥 = 𝑦 ∧ 𝜓)) |
7 | 4, 6 | mpbiran 705 | . 2 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜓) ↔ 𝜓) |
8 | 3, 7 | bitri 274 | 1 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 ∃wex 1779 Ⅎwnf 1783 |
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 1911 ax-6 1969 ax-7 2009 ax-12 2169 ax-13 2369 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1780 df-nf 1784 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |