Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > equsexvw | Structured version Visualization version GIF version |
Description: Version of equsexv 2269 with a disjoint variable condition, and of equsex 2440 with two disjoint variable conditions, which requires fewer axioms. See also the dual form equsalvw 2010. (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 320 | . . . 4 ⊢ (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓)) |
4 | 3 | equsalvw 2010 | . . 3 ⊢ (∀𝑥(𝑥 = 𝑦 → ¬ 𝜑) ↔ ¬ 𝜓) |
5 | 1, 4 | bitr3i 279 | . 2 ⊢ (¬ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ¬ 𝜓) |
6 | 5 | con4bii 323 | 1 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 398 ∀wal 1535 ∃wex 1780 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1781 |
This theorem is referenced by: equvinv 2036 cleljust 2123 sbelx 2255 cleljustab 2804 sbhypf 3554 axsepgfromrep 5203 dfid3 5464 opeliunxp 5621 imai 5944 coi1 6117 opabex3d 7668 opabex3rd 7669 opabex3 7670 fsplit 7814 fsplitOLD 7815 mapsnend 8590 dfac5lem1 9551 dfac5lem3 9553 dffix2 33368 sscoid 33376 elfuns 33378 pmapglb 36908 polval2N 37044 opeliun2xp 44388 |
Copyright terms: Public domain | W3C validator |