|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > equsex | Structured version Visualization version GIF version | ||
| Description: An equivalence related to implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2376. See equsexvw 2003 and equsexv 2267 for versions with disjoint variable conditions proved from fewer axioms. See also the dual form equsal 2421. See equsexALT 2423 for an alternate proof. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 6-Feb-2018.) (New usage is discouraged.) | 
| Ref | Expression | 
|---|---|
| equsal.1 | ⊢ Ⅎ𝑥𝜓 | 
| equsal.2 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | 
| Ref | Expression | 
|---|---|
| equsex | ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | equsal.1 | . . 3 ⊢ Ⅎ𝑥𝜓 | |
| 2 | equsal.2 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
| 3 | 2 | biimpa 476 | . . 3 ⊢ ((𝑥 = 𝑦 ∧ 𝜑) → 𝜓) | 
| 4 | 1, 3 | exlimi 2216 | . 2 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → 𝜓) | 
| 5 | 1, 2 | equsal 2421 | . . 3 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓) | 
| 6 | equs4 2420 | . . 3 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) | |
| 7 | 5, 6 | sylbir 235 | . 2 ⊢ (𝜓 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) | 
| 8 | 4, 7 | impbii 209 | 1 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∀wal 1537 ∃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: equsexh 2425 sb5rf 2471 | 
| Copyright terms: Public domain | W3C validator |