![]() |
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 2371. See equsexvw 2009 and equsexv 2260 for versions with disjoint variable conditions proved from fewer axioms. See also the dual form equsal 2416. See equsexALT 2418 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 478 | . . 3 ⊢ ((𝑥 = 𝑦 ∧ 𝜑) → 𝜓) |
4 | 1, 3 | exlimi 2211 | . 2 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → 𝜓) |
5 | 1, 2 | equsal 2416 | . . 3 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓) |
6 | equs4 2415 | . . 3 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) | |
7 | 5, 6 | sylbir 234 | . 2 ⊢ (𝜓 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) |
8 | 4, 7 | impbii 208 | 1 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 ∀wal 1540 ∃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: equsexh 2420 sb5rf 2466 |
Copyright terms: Public domain | W3C validator |