![]() |
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. See equsexvw 2111 and equsexv 2301 for versions with disjoint variable conditions proved from fewer axioms. See also the dual form equsal 2437. See equsexALT 2439 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.) |
Ref | Expression |
---|---|
equsal.1 | ⊢ Ⅎ𝑥𝜓 |
equsal.2 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
equsex | ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | equsal.1 | . . 3 ⊢ Ⅎ𝑥𝜓 | |
2 | equsal.2 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
3 | 2 | biimpa 470 | . . 3 ⊢ ((𝑥 = 𝑦 ∧ 𝜑) → 𝜓) |
4 | 1, 3 | exlimi 2262 | . 2 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → 𝜓) |
5 | 1, 2 | equsal 2437 | . . 3 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓) |
6 | equs4 2436 | . . 3 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) | |
7 | 5, 6 | sylbir 227 | . 2 ⊢ (𝜓 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) |
8 | 4, 7 | impbii 201 | 1 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 386 ∀wal 1656 ∃wex 1880 Ⅎwnf 1884 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-12 2222 ax-13 2390 |
This theorem depends on definitions: df-bi 199 df-an 387 df-ex 1881 df-nf 1885 |
This theorem is referenced by: equsexh 2441 sb5rf 2553 |
Copyright terms: Public domain | W3C validator |