New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > excom | GIF version |
Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) (Revised by Wolf Lammen to remove dependency on ax-11 1746 ax-6 1729 ax-9 1654 ax-8 1675 and ax-17 1616, 8-Jan-2018.) |
Ref | Expression |
---|---|
excom | ⊢ (∃x∃yφ ↔ ∃y∃xφ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | alcom 1737 | . . . 4 ⊢ (∀x∀y ¬ φ ↔ ∀y∀x ¬ φ) | |
2 | 1 | notbii 287 | . . 3 ⊢ (¬ ∀x∀y ¬ φ ↔ ¬ ∀y∀x ¬ φ) |
3 | exnal 1574 | . . 3 ⊢ (∃x ¬ ∀y ¬ φ ↔ ¬ ∀x∀y ¬ φ) | |
4 | exnal 1574 | . . 3 ⊢ (∃y ¬ ∀x ¬ φ ↔ ¬ ∀y∀x ¬ φ) | |
5 | 2, 3, 4 | 3bitr4i 268 | . 2 ⊢ (∃x ¬ ∀y ¬ φ ↔ ∃y ¬ ∀x ¬ φ) |
6 | df-ex 1542 | . . 3 ⊢ (∃yφ ↔ ¬ ∀y ¬ φ) | |
7 | 6 | exbii 1582 | . 2 ⊢ (∃x∃yφ ↔ ∃x ¬ ∀y ¬ φ) |
8 | df-ex 1542 | . . 3 ⊢ (∃xφ ↔ ¬ ∀x ¬ φ) | |
9 | 8 | exbii 1582 | . 2 ⊢ (∃y∃xφ ↔ ∃y ¬ ∀x ¬ φ) |
10 | 5, 7, 9 | 3bitr4i 268 | 1 ⊢ (∃x∃yφ ↔ ∃y∃xφ) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 176 ∀wal 1540 ∃wex 1541 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 ax-5 1557 ax-7 1734 |
This theorem depends on definitions: df-bi 177 df-ex 1542 |
This theorem is referenced by: excomim 1742 excom13 1743 exrot3 1744 ee4anv 1915 2exsb 2132 2euex 2276 2eu1 2284 2eu4 2287 rexcomf 2770 gencbvex 2901 euind 3023 sbccomlem 3116 elpw11c 4147 elpw121c 4148 elpw131c 4149 elpw141c 4150 elpw151c 4151 elpw161c 4152 elpw171c 4153 elpw181c 4154 elpw191c 4155 elpw1101c 4156 elpw1111c 4157 eluni1g 4172 opkelcokg 4261 opkelimagekg 4271 dfimak2 4298 insklem 4304 ndisjrelk 4323 dfpw2 4327 dfaddc2 4381 dfnnc2 4395 elsuc 4413 nnsucelrlem1 4424 ltfinex 4464 ssfin 4470 eqpwrelk 4478 eqpw1relk 4479 ncfinraiselem2 4480 ncfinlowerlem1 4482 eqtfinrelk 4486 evenfinex 4503 oddfinex 4504 evenodddisjlem1 4515 nnadjoinlem1 4519 nnpweqlem1 4522 srelk 4524 sfintfinlem1 4531 tfinnnlem1 4533 spfinex 4537 vfinspsslem1 4550 dfop2lem1 4573 el1st 4729 setconslem1 4731 setconslem2 4732 setconslem3 4733 setconslem7 4737 df1st2 4738 dfswap2 4741 brswap2 4860 dmuni 4914 dm0rn0 4921 elimapw11c 4948 dmcoss 4971 dmcosseq 4973 rnuni 5038 rnco 5087 coass 5097 df2nd2 5111 cnvswap 5510 cnvsi 5518 dmsi 5519 oprabid 5550 dfoprab2 5558 brsnsi1 5775 brimage 5793 addcfnex 5824 pw1fnf1o 5855 ceexlem1 6173 ce0nnul 6177 el2c 6191 taddc 6229 tcfnex 6244 csucex 6259 nmembers1lem1 6268 nchoicelem11 6299 nchoicelem16 6304 fnfreclem3 6319 |
Copyright terms: Public domain | W3C validator |