![]() |
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 1914, ax-6 1972, ax-7 2012, ax-10 2138, ax-12 2172. (Revised by Wolf Lammen, 8-Jan-2018.) (Proof shortened by Wolf Lammen, 22-Aug-2020.) |
Ref | Expression |
---|---|
excom | ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | alcom 2157 | . . 3 ⊢ (∀𝑥∀𝑦 ¬ 𝜑 ↔ ∀𝑦∀𝑥 ¬ 𝜑) | |
2 | 1 | notbii 320 | . 2 ⊢ (¬ ∀𝑥∀𝑦 ¬ 𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑) |
3 | 2exnaln 1832 | . 2 ⊢ (∃𝑥∃𝑦𝜑 ↔ ¬ ∀𝑥∀𝑦 ¬ 𝜑) | |
4 | 2exnaln 1832 | . 2 ⊢ (∃𝑦∃𝑥𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑) | |
5 | 2, 3, 4 | 3bitr4i 303 | 1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205 ∀wal 1540 ∃wex 1782 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-11 2155 |
This theorem depends on definitions: df-bi 206 df-ex 1783 |
This theorem is referenced by: excomim 2164 excom13 2165 exrot3 2166 eeor 2330 ee4anv 2348 2sb8ef 2353 sbel2x 2473 2sb8e 2534 2euexv 2632 2euex 2642 2eu4 2655 rexcom4 3274 rexcomf 3289 cgsex4gOLD 3494 gencbvex 3507 euind 3687 sbccomlem 3831 elvvv 5712 dmuni 5875 dm0rn0 5885 dmcosseq 5933 rnco 6209 coass 6222 oprabidw 7393 oprabid 7394 dfoprab2 7420 uniuni 7701 opabex3d 7903 opabex3rd 7904 opabex3 7905 frxp 8063 domen 8908 xpassen 9017 scott0 9829 dfac5lem1 10066 dfac5lem4 10069 cflem 10189 ltexprlem1 10979 ltexprlem4 10982 fsumcom2 15666 fprodcom2 15874 gsumval3eu 19688 dprd2d2 19830 cnvoprabOLD 31679 eldm3 34373 dfdm5 34386 dfrn5 34387 elfuns 34529 dfiota3 34537 brimg 34551 funpartlem 34556 bj-19.12 35255 bj-nnflemee 35257 bj-restuni 35597 sbccom2lem 36612 diblsmopel 39663 dicelval3 39672 dihjatcclem4 39913 19.9dev 40659 nnoeomeqom 41676 pm11.6 42746 ax6e2ndeq 42915 e2ebind 42919 ax6e2ndeqVD 43265 e2ebindVD 43268 e2ebindALT 43285 ax6e2ndeqALT 43287 ich2ex 45734 ichexmpl1 45735 elsprel 45741 eliunxp2 46483 |
Copyright terms: Public domain | W3C validator |