Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > excom | Structured version Visualization version GIF version |
Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) Remove dependencies on ax-5 1827, ax-6 1875, ax-7 1922, ax-10 2006, ax-12 2034. (Revised by Wolf Lammen, 8-Jan-2018.) (Proof shortened by Wolf Lammen, 22-Aug-2020.) |
Ref | Expression |
---|---|
excom | ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | alcom 2024 | . . 3 ⊢ (∀𝑥∀𝑦 ¬ 𝜑 ↔ ∀𝑦∀𝑥 ¬ 𝜑) | |
2 | 1 | notbii 309 | . 2 ⊢ (¬ ∀𝑥∀𝑦 ¬ 𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑) |
3 | 2exnaln 1746 | . 2 ⊢ (∃𝑥∃𝑦𝜑 ↔ ¬ ∀𝑥∀𝑦 ¬ 𝜑) | |
4 | 2exnaln 1746 | . 2 ⊢ (∃𝑦∃𝑥𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑) | |
5 | 2, 3, 4 | 3bitr4i 291 | 1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 195 ∀wal 1473 ∃wex 1695 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-11 2021 |
This theorem depends on definitions: df-bi 196 df-ex 1696 |
This theorem is referenced by: excomim 2030 excom13 2031 exrot3 2032 ee4anv 2172 sbel2x 2447 2sb8e 2455 2euex 2532 2eu4 2544 rexcomf 3078 gencbvex 3223 euind 3360 sbccomlem 3475 opelopabsbALT 4909 elvvv 5101 dmuni 5256 dm0rn0 5263 dmcosseq 5308 elres 5355 rnco 5558 coass 5571 oprabid 6576 dfoprab2 6599 uniuni 6865 opabex3d 7037 opabex3 7038 frxp 7174 domen 7854 xpassen 7939 scott0 8632 dfac5lem1 8829 dfac5lem4 8832 cflem 8951 ltexprlem1 9737 ltexprlem4 9740 fsumcom2 14347 fsumcom2OLD 14348 fprodcom2 14553 fprodcom2OLD 14554 gsumval3eu 18128 dprd2d2 18266 usgraedg4 25916 cnvoprab 28886 eldm3 30905 dfdm5 30921 dfrn5 30922 elfuns 31192 dfiota3 31200 brimg 31214 funpartlem 31219 bj-rexcom4 32063 bj-restuni 32231 sbccom2lem 33099 diblsmopel 35478 dicelval3 35487 dihjatcclem4 35728 pm11.6 37614 ax6e2ndeq 37796 e2ebind 37800 ax6e2ndeqVD 38167 e2ebindVD 38170 e2ebindALT 38187 ax6e2ndeqALT 38189 eliunxp2 41905 |
Copyright terms: Public domain | W3C validator |