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 1932 and equsexv 2109 for versions with dv conditions proved from fewer axioms. See also the dual form equsal 2291. See equsexALT 2293 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 501 | . . 3 ⊢ ((𝑥 = 𝑦 ∧ 𝜑) → 𝜓) |
4 | 1, 3 | exlimi 2086 | . 2 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → 𝜓) |
5 | 1, 2 | equsal 2291 | . . 3 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓) |
6 | equs4 2290 | . . 3 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) | |
7 | 5, 6 | sylbir 225 | . 2 ⊢ (𝜓 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) |
8 | 4, 7 | impbii 199 | 1 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 384 ∀wal 1481 ∃wex 1704 Ⅎwnf 1708 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-12 2047 ax-13 2246 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-ex 1705 df-nf 1710 |
This theorem is referenced by: equsexh 2295 sb5rf 2422 |
Copyright terms: Public domain | W3C validator |