![]() |
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 2417. This proves the result directly, instead of as a corollary of equsal 2416 via equs4 2415. Note in particular that only existential quantifiers appear in the proof and that the only step requiring ax-13 2371 is ax6e 2382. This proof mimics that of equsal 2416 (in particular, note that pm5.32i 576, exbii 1851, 19.41 2229, mpbiran 708 correspond respectively to pm5.74i 271, albii 1822, 19.23 2205, a1bi 363). (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 576 | . . 3 ⊢ ((𝑥 = 𝑦 ∧ 𝜑) ↔ (𝑥 = 𝑦 ∧ 𝜓)) |
3 | 2 | exbii 1851 | . 2 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜓)) |
4 | ax6e 2382 | . . 3 ⊢ ∃𝑥 𝑥 = 𝑦 | |
5 | equsal.1 | . . . 4 ⊢ Ⅎ𝑥𝜓 | |
6 | 5 | 19.41 2229 | . . 3 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜓) ↔ (∃𝑥 𝑥 = 𝑦 ∧ 𝜓)) |
7 | 4, 6 | mpbiran 708 | . 2 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜓) ↔ 𝜓) |
8 | 3, 7 | bitri 275 | 1 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 ∃wex 1782 Ⅎwnf 1786 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-12 2172 ax-13 2371 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-nf 1787 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |