|   | 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 2422. This proves the result directly, instead of as a corollary of equsal 2421 via equs4 2420. Note in particular that only existential quantifiers appear in the proof and that the only step requiring ax-13 2376 is ax6e 2387. This proof mimics that of equsal 2421 (in particular, note that pm5.32i 574, exbii 1847, 19.41 2234, mpbiran 709 correspond respectively to pm5.74i 271, albii 1818, 19.23 2210, a1bi 362). (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 574 | . . 3 ⊢ ((𝑥 = 𝑦 ∧ 𝜑) ↔ (𝑥 = 𝑦 ∧ 𝜓)) | 
| 3 | 2 | exbii 1847 | . 2 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜓)) | 
| 4 | ax6e 2387 | . . 3 ⊢ ∃𝑥 𝑥 = 𝑦 | |
| 5 | equsal.1 | . . . 4 ⊢ Ⅎ𝑥𝜓 | |
| 6 | 5 | 19.41 2234 | . . 3 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜓) ↔ (∃𝑥 𝑥 = 𝑦 ∧ 𝜓)) | 
| 7 | 4, 6 | mpbiran 709 | . 2 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜓) ↔ 𝜓) | 
| 8 | 3, 7 | bitri 275 | 1 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∃wex 1778 Ⅎwnf 1782 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-12 2176 ax-13 2376 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1779 df-nf 1783 | 
| This theorem is referenced by: (None) | 
| Copyright terms: Public domain | W3C validator |