| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > equsexvw | Structured version Visualization version GIF version | ||
| Description: Version of equsexv 2268 with a disjoint variable condition, and of equsex 2423 with two disjoint variable conditions, which requires fewer axioms. See also the dual form equsalvw 2003. (Contributed by BJ, 31-May-2019.) (Proof shortened by Wolf Lammen, 23-Oct-2023.) |
| Ref | Expression |
|---|---|
| equsalvw.1 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
| Ref | Expression |
|---|---|
| equsexvw | ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | alinexa 1843 | . . 3 ⊢ (∀𝑥(𝑥 = 𝑦 → ¬ 𝜑) ↔ ¬ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) | |
| 2 | equsalvw.1 | . . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
| 3 | 2 | notbid 318 | . . . 4 ⊢ (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓)) |
| 4 | 3 | equsalvw 2003 | . . 3 ⊢ (∀𝑥(𝑥 = 𝑦 → ¬ 𝜑) ↔ ¬ 𝜓) |
| 5 | 1, 4 | bitr3i 277 | . 2 ⊢ (¬ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ¬ 𝜓) |
| 6 | 5 | con4bii 321 | 1 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∀wal 1538 ∃wex 1779 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 |
| This theorem is referenced by: equvinv 2028 cleljust 2117 sbelx 2253 cleljustab 2717 sbhypfOLD 3545 axsepgfromrep 5294 dfid3 5581 opeliunxp 5752 opeliun2xp 5753 imai 6092 coi1 6282 opabex3d 7990 opabex3rd 7991 opabex3 7992 fsplit 8142 mapsnend 9076 dfac5lem1 10163 dfac5lem3 10165 dffix2 35906 sscoid 35914 elfuns 35916 pmapglb 39772 polval2N 39908 tfsconcat0i 43358 |
| Copyright terms: Public domain | W3C validator |