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 2431. This proves the result directly, instead of as a corollary of equsal 2430 via equs4 2429. Note in particular that only existential quantifiers appear in the proof and that the only step requiring ax-13 2381 is ax6e 2392. This proof mimics that of equsal 2430 (in particular, note that pm5.32i 575, exbii 1839, 19.41 2227, mpbiran 705 correspond respectively to pm5.74i 272, albii 1811, 19.23 2201, a1bi 364). (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 575 | . . 3 ⊢ ((𝑥 = 𝑦 ∧ 𝜑) ↔ (𝑥 = 𝑦 ∧ 𝜓)) |
3 | 2 | exbii 1839 | . 2 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜓)) |
4 | ax6e 2392 | . . 3 ⊢ ∃𝑥 𝑥 = 𝑦 | |
5 | equsal.1 | . . . 4 ⊢ Ⅎ𝑥𝜓 | |
6 | 5 | 19.41 2227 | . . 3 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜓) ↔ (∃𝑥 𝑥 = 𝑦 ∧ 𝜓)) |
7 | 4, 6 | mpbiran 705 | . 2 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜓) ↔ 𝜓) |
8 | 3, 7 | bitri 276 | 1 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 ∃wex 1771 Ⅎwnf 1775 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-12 2167 ax-13 2381 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-nf 1776 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |