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 2440. This proves the result directly, instead of as a corollary of equsal 2439 via equs4 2438. Note in particular that only existential quantifiers appear in the proof and that the only step requiring ax-13 2390 is ax6e 2401. This proof mimics that of equsal 2439 (in particular, note that pm5.32i 577, exbii 1848, 19.41 2237, mpbiran 707 correspond respectively to pm5.74i 273, albii 1820, 19.23 2211, a1bi 365). (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 577 | . . 3 ⊢ ((𝑥 = 𝑦 ∧ 𝜑) ↔ (𝑥 = 𝑦 ∧ 𝜓)) |
3 | 2 | exbii 1848 | . 2 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜓)) |
4 | ax6e 2401 | . . 3 ⊢ ∃𝑥 𝑥 = 𝑦 | |
5 | equsal.1 | . . . 4 ⊢ Ⅎ𝑥𝜓 | |
6 | 5 | 19.41 2237 | . . 3 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜓) ↔ (∃𝑥 𝑥 = 𝑦 ∧ 𝜓)) |
7 | 4, 6 | mpbiran 707 | . 2 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜓) ↔ 𝜓) |
8 | 3, 7 | bitri 277 | 1 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∃wex 1780 Ⅎwnf 1784 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-12 2177 ax-13 2390 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1781 df-nf 1785 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |