![]() |
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 1888, ax-6 1947, ax-7 1992, ax-10 2112, ax-12 2141. (Revised by Wolf Lammen, 8-Jan-2018.) (Proof shortened by Wolf Lammen, 22-Aug-2020.) |
Ref | Expression |
---|---|
excom | ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | alcom 2128 | . . 3 ⊢ (∀𝑥∀𝑦 ¬ 𝜑 ↔ ∀𝑦∀𝑥 ¬ 𝜑) | |
2 | 1 | notbii 321 | . 2 ⊢ (¬ ∀𝑥∀𝑦 ¬ 𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑) |
3 | 2exnaln 1810 | . 2 ⊢ (∃𝑥∃𝑦𝜑 ↔ ¬ ∀𝑥∀𝑦 ¬ 𝜑) | |
4 | 2exnaln 1810 | . 2 ⊢ (∃𝑦∃𝑥𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑) | |
5 | 2, 3, 4 | 3bitr4i 304 | 1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 207 ∀wal 1520 ∃wex 1761 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-11 2126 |
This theorem depends on definitions: df-bi 208 df-ex 1762 |
This theorem is referenced by: excomim 2134 excom13 2135 exrot3 2136 ee4anv 2328 2sb8ev 2331 2sb8evOLD 2332 sbel2x 2456 2sb8e 2530 2euexv 2686 2euex 2696 2eu4 2711 rexcom4 3213 rexcomOLD 3317 rexcomf 3319 cgsex4g 3482 gencbvex 3492 euind 3649 sbccomlem 3781 opelopabsbALT 5306 elvvv 5513 dmuni 5669 dm0rn0 5679 dmcosseq 5725 rnco 5980 coass 5993 oprabid 7047 dfoprab2 7071 uniuni 7341 opabex3d 7522 opabex3rd 7523 opabex3 7524 frxp 7673 domen 8370 xpassen 8458 scott0 9161 dfac5lem1 9395 dfac5lem4 9398 cflem 9514 ltexprlem1 10304 ltexprlem4 10307 fsumcom2 14962 fprodcom2 15171 gsumval3eu 18745 dprd2d2 18883 cnvoprabOLD 30144 eldm3 32606 dfdm5 32625 dfrn5 32626 elfuns 32986 dfiota3 32994 brimg 33008 funpartlem 33013 bj-19.12 33884 bj-nnflemee 33886 bj-restuni 34006 sbccom2lem 34953 diblsmopel 37857 dicelval3 37866 dihjatcclem4 38107 pm11.6 40281 ax6e2ndeq 40451 e2ebind 40455 ax6e2ndeqVD 40801 e2ebindVD 40804 e2ebindALT 40821 ax6e2ndeqALT 40823 ich2ex 43131 ichexmpl1 43133 elsprel 43139 eliunxp2 43880 |
Copyright terms: Public domain | W3C validator |