| 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 1910, ax-6 1967, ax-7 2007, ax-10 2141, ax-12 2177. (Revised by Wolf Lammen, 8-Jan-2018.) (Proof shortened by Wolf Lammen, 22-Aug-2020.) |
| Ref | Expression |
|---|---|
| excom | ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | alcom 2159 | . . 3 ⊢ (∀𝑥∀𝑦 ¬ 𝜑 ↔ ∀𝑦∀𝑥 ¬ 𝜑) | |
| 2 | 1 | notbii 320 | . 2 ⊢ (¬ ∀𝑥∀𝑦 ¬ 𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑) |
| 3 | 2exnaln 1829 | . 2 ⊢ (∃𝑥∃𝑦𝜑 ↔ ¬ ∀𝑥∀𝑦 ¬ 𝜑) | |
| 4 | 2exnaln 1829 | . 2 ⊢ (∃𝑦∃𝑥𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑) | |
| 5 | 2, 3, 4 | 3bitr4i 303 | 1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 ↔ wb 206 ∀wal 1538 ∃wex 1779 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-11 2157 |
| This theorem depends on definitions: df-bi 207 df-ex 1780 |
| This theorem is referenced by: excomim 2163 excom13 2164 exrot3 2165 eeor 2335 ee4anv 2353 ee4anvOLD 2354 2sb8ef 2359 sbel2x 2479 2sb8e 2535 2euexv 2631 2euex 2641 2eu4 2655 rexcom4 3288 rexcomf 3303 gencbvex 3541 euind 3730 sbccomlemOLD 3870 elvvv 5761 dmuni 5925 dm0rn0 5935 dmcosseqOLD 5988 cnvopab 6157 rnco 6272 coass 6285 oprabidw 7462 oprabid 7463 dfoprab2 7491 uniuni 7782 opabex3d 7990 opabex3rd 7991 opabex3 7992 frxp 8151 domen 9002 xpassen 9106 scott0 9926 dfac5lem1 10163 dfac5lem4OLD 10168 cflemOLD 10286 ltexprlem1 11076 ltexprlem4 11079 fsumcom2 15810 fprodcom2 16020 gsumval3eu 19922 dprd2d2 20064 eldm3 35761 dfdm5 35773 dfrn5 35774 elfuns 35916 dfiota3 35924 brimg 35938 funpartlem 35943 bj-19.12 36762 bj-nnflemee 36764 bj-restuni 37098 sbccom2lem 38131 diblsmopel 41173 dicelval3 41182 dihjatcclem4 41423 19.9dev 42253 nnoeomeqom 43325 pm11.6 44411 ax6e2ndeq 44579 e2ebind 44583 ax6e2ndeqVD 44929 e2ebindVD 44932 e2ebindALT 44949 ax6e2ndeqALT 44951 ich2ex 47455 ichexmpl1 47456 elsprel 47462 eliunxp2 48250 |
| Copyright terms: Public domain | W3C validator |