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 2434 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 1834 | . . 3 ⊢ (∀𝑥(𝑥 = 𝑦 → ¬ 𝜑) ↔ ¬ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) | |
2 | equsalvw.1 | . . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
3 | 2 | notbid 319 | . . . 4 ⊢ (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓)) |
4 | 3 | equsalvw 2001 | . . 3 ⊢ (∀𝑥(𝑥 = 𝑦 → ¬ 𝜑) ↔ ¬ 𝜓) |
5 | 1, 4 | bitr3i 278 | . 2 ⊢ (¬ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ¬ 𝜓) |
6 | 5 | con4bii 322 | 1 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∧ wa 396 ∀wal 1526 ∃wex 1771 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 |
This theorem is referenced by: equvinv 2027 cleljust 2114 sbelx 2246 cleljustab 2802 sbhypf 3553 axsepgfromrep 5193 dfid3 5456 opeliunxp 5613 imai 5936 coi1 6109 opabex3d 7657 opabex3rd 7658 opabex3 7659 fsplit 7803 fsplitOLD 7804 mapsnend 8577 dfac5lem1 9538 dfac5lem3 9540 dffix2 33264 sscoid 33272 elfuns 33274 pmapglb 36788 polval2N 36924 opeliun2xp 44279 |
Copyright terms: Public domain | W3C validator |