![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rexcom4 | Structured version Visualization version GIF version |
Description: Commutation of restricted and unrestricted existential quantifiers. (Contributed by NM, 12-Apr-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) Reduce axiom dependencies. (Revised by BJ, 13-Jun-2019.) |
Ref | Expression |
---|---|
rexcom4 | ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exdistr 1959 | . 2 ⊢ (∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ ∃𝑦𝜑)) | |
2 | df-rex 3072 | . . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
3 | 2 | exbii 1851 | . . 3 ⊢ (∃𝑦∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
4 | excom 2163 | . . 3 ⊢ (∃𝑦∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
5 | 3, 4 | bitri 275 | . 2 ⊢ (∃𝑦∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ 𝜑)) |
6 | df-rex 3072 | . 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ ∃𝑦𝜑)) | |
7 | 1, 5, 6 | 3bitr4ri 304 | 1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 397 ∃wex 1782 ∈ wcel 2107 ∃wrex 3071 |
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-5 1914 ax-11 2155 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-rex 3072 |
This theorem is referenced by: rexcomOLD 3289 rexcom4a 3290 2ex2rexrot 3296 reuind 3748 uni0b 4936 iuncom4 5004 dfiun2g 5032 dfiun2gOLD 5033 iunn0 5069 iunxiun 5099 iinexg 5340 inuni 5342 iunopab 5558 iunopabOLD 5559 xpiundi 5744 xpiundir 5745 cnvuni 5884 dmiun 5911 dmopab2rex 5915 elsnres 6019 rniun 6144 xpdifid 6164 imaco 6247 coiun 6252 abrexco 7238 imaiun 7239 fliftf 7307 imaeqsexv 7355 imaeqexov 7640 fiun 7924 f1iun 7925 oprabrexex2 7960 releldm2 8024 oarec 8558 omeu 8581 eroveu 8802 brttrcl2 9705 dfac5lem2 10115 genpass 11000 supaddc 12177 supadd 12178 supmul1 12179 supmullem2 12181 supmul 12182 pceu 16775 4sqlem12 16885 mreiincl 17536 psgneu 19367 ntreq0 22563 unisngl 23013 metrest 24015 metuel2 24056 nosupno 27186 nosupfv 27189 noinfno 27201 noinffv 27204 elold 27344 lrrecfr 27407 sleadd1 27452 addsuniflem 27464 addsasslem1 27466 addsasslem2 27467 mulsuniflem 27584 addsdilem1 27586 addsdilem2 27587 mulsasslem1 27598 mulsasslem2 27599 istrkg2ld 27691 fpwrelmapffslem 31935 omssubaddlem 33236 omssubadd 33237 bnj906 33879 satfdm 34298 dmopab3rexdif 34334 bj-elsngl 35787 bj-restn0 35909 ismblfin 36467 itg2addnclem3 36479 sdclem1 36549 eldmqs1cossres 37467 prter2 37689 lshpsmreu 37917 islpln5 38344 islvol5 38388 cdlemftr3 39374 mapdpglem3 40484 hdmapglem7a 40736 diophrex 41446 imaiun1 42335 coiun1 42336 grumnudlem 42977 upbdrech 43950 |
Copyright terms: Public domain | W3C validator |