![]() |
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 1905, ax-6 1963, ax-7 2003, ax-10 2129, ax-12 2166. (Revised by Wolf Lammen, 8-Jan-2018.) (Proof shortened by Wolf Lammen, 22-Aug-2020.) |
Ref | Expression |
---|---|
excom | ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | alcom 2148 | . . 3 ⊢ (∀𝑥∀𝑦 ¬ 𝜑 ↔ ∀𝑦∀𝑥 ¬ 𝜑) | |
2 | 1 | notbii 319 | . 2 ⊢ (¬ ∀𝑥∀𝑦 ¬ 𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑) |
3 | 2exnaln 1823 | . 2 ⊢ (∃𝑥∃𝑦𝜑 ↔ ¬ ∀𝑥∀𝑦 ¬ 𝜑) | |
4 | 2exnaln 1823 | . 2 ⊢ (∃𝑦∃𝑥𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑) | |
5 | 2, 3, 4 | 3bitr4i 302 | 1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205 ∀wal 1531 ∃wex 1773 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-11 2146 |
This theorem depends on definitions: df-bi 206 df-ex 1774 |
This theorem is referenced by: excomim 2152 excom13 2153 exrot3 2154 eeor 2323 ee4anv 2341 2sb8ef 2346 sbel2x 2467 2sb8e 2523 2euexv 2619 2euex 2629 2eu4 2643 rexcom4 3275 rexcomf 3290 cgsex4gOLDOLD 3511 gencbvex 3525 euind 3716 sbccomlem 3860 elvvv 5753 dmuni 5917 dm0rn0 5927 dmcosseq 5976 cnvopab 6144 rnco 6258 coass 6271 oprabidw 7450 oprabid 7451 dfoprab2 7478 uniuni 7765 opabex3d 7970 opabex3rd 7971 opabex3 7972 frxp 8131 domen 8982 xpassen 9091 scott0 9911 dfac5lem1 10148 dfac5lem4 10151 cflem 10271 ltexprlem1 11061 ltexprlem4 11064 fsumcom2 15756 fprodcom2 15964 gsumval3eu 19871 dprd2d2 20013 cnvoprabOLD 32584 eldm3 35483 dfdm5 35496 dfrn5 35497 elfuns 35639 dfiota3 35647 brimg 35661 funpartlem 35666 bj-19.12 36366 bj-nnflemee 36368 bj-restuni 36704 sbccom2lem 37725 diblsmopel 40771 dicelval3 40780 dihjatcclem4 41021 19.9dev 41832 nnoeomeqom 42880 pm11.6 43968 ax6e2ndeq 44137 e2ebind 44141 ax6e2ndeqVD 44487 e2ebindVD 44490 e2ebindALT 44507 ax6e2ndeqALT 44509 ich2ex 46942 ichexmpl1 46943 elsprel 46949 eliunxp2 47580 |
Copyright terms: Public domain | W3C validator |