![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > equsexvw | Structured version Visualization version GIF version |
Description: Version of equsexv 2260 with a disjoint variable condition, and of equsex 2418 with two disjoint variable conditions, which requires fewer axioms. See also the dual form equsalvw 2008. (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 1846 | . . 3 ⊢ (∀𝑥(𝑥 = 𝑦 → ¬ 𝜑) ↔ ¬ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) | |
2 | equsalvw.1 | . . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
3 | 2 | notbid 318 | . . . 4 ⊢ (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓)) |
4 | 3 | equsalvw 2008 | . . 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 205 ∧ wa 397 ∀wal 1540 ∃wex 1782 |
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 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 |
This theorem is referenced by: equvinv 2033 cleljust 2116 sbelx 2246 cleljustab 2713 sbhypfOLD 3539 axsepgfromrep 5296 dfid3 5576 opeliunxp 5741 imai 6070 coi1 6258 opabex3d 7947 opabex3rd 7948 opabex3 7949 fsplit 8098 mapsnend 9032 dfac5lem1 10114 dfac5lem3 10116 dffix2 34815 sscoid 34823 elfuns 34825 pmapglb 38579 polval2N 38715 tfsconcat0i 42028 opeliun2xp 46910 |
Copyright terms: Public domain | W3C validator |