![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > equsexvw | Structured version Visualization version GIF version |
Description: Version of equsexv 2266 with a disjoint variable condition, and of equsex 2421 with two disjoint variable conditions, which requires fewer axioms. See also the dual form equsalvw 2001. (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 1840 | . . 3 ⊢ (∀𝑥(𝑥 = 𝑦 → ¬ 𝜑) ↔ ¬ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) | |
2 | equsalvw.1 | . . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
3 | 2 | notbid 318 | . . . 4 ⊢ (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓)) |
4 | 3 | equsalvw 2001 | . . 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 1535 ∃wex 1776 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 |
This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1777 |
This theorem is referenced by: equvinv 2026 cleljust 2115 sbelx 2251 cleljustab 2715 sbhypfOLD 3545 axsepgfromrep 5300 dfid3 5586 opeliunxp 5756 imai 6094 coi1 6284 opabex3d 7989 opabex3rd 7990 opabex3 7991 fsplit 8141 mapsnend 9075 dfac5lem1 10161 dfac5lem3 10163 dffix2 35887 sscoid 35895 elfuns 35897 pmapglb 39753 polval2N 39889 tfsconcat0i 43335 opeliun2xp 48178 |
Copyright terms: Public domain | W3C validator |