Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > equsexvw | Structured version Visualization version GIF version |
Description: Version of equsexv 2259 with a disjoint variable condition, and of equsex 2431 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 2245 cleljustab 2799 sbhypf 3550 axsepgfromrep 5192 dfid3 5455 opeliunxp 5612 imai 5935 coi1 6108 opabex3d 7655 opabex3rd 7656 opabex3 7657 fsplit 7801 fsplitOLD 7802 mapsnend 8576 dfac5lem1 9537 dfac5lem3 9539 dffix2 33263 sscoid 33271 elfuns 33273 pmapglb 36786 polval2N 36922 opeliun2xp 44309 |
Copyright terms: Public domain | W3C validator |