| 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 1954 | . 2 ⊢ (∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ ∃𝑦𝜑)) | |
| 2 | df-rex 3071 | . . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
| 3 | 2 | exbii 1848 | . . 3 ⊢ (∃𝑦∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
| 4 | excom 2162 | . . 3 ⊢ (∃𝑦∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
| 5 | 3, 4 | bitri 275 | . 2 ⊢ (∃𝑦∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ 𝜑)) |
| 6 | df-rex 3071 | . 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ ∃𝑦𝜑)) | |
| 7 | 1, 5, 6 | 3bitr4ri 304 | 1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∧ wa 395 ∃wex 1779 ∈ wcel 2108 ∃wrex 3070 |
| 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-5 1910 ax-11 2157 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-rex 3071 |
| This theorem is referenced by: rexcomOLD 3291 rexcom4a 3292 2ex2rexrot 3298 reuind 3759 uni0b 4933 iuncom4 5000 dfiun2g 5030 dfiun2gOLD 5031 iunn0 5067 iunxiun 5097 iinexg 5348 inuni 5350 iunopab 5564 iunopabOLD 5565 xpiundi 5756 xpiundir 5757 cnvuni 5897 dmiun 5924 dmopab2rex 5928 elsnres 6039 rniun 6167 xpdifid 6188 imaco 6271 coiun 6276 abrexco 7264 imaiun 7265 fliftf 7335 imaeqsexvOLD 7383 imaeqexov 7671 fiun 7967 f1iun 7968 oprabrexex2 8003 releldm2 8068 oarec 8600 omeu 8623 eroveu 8852 brttrcl2 9754 dfac5lem2 10164 genpass 11049 supaddc 12235 supadd 12236 supmul1 12237 supmullem2 12239 supmul 12240 pceu 16884 4sqlem12 16994 mreiincl 17639 psgneu 19524 ntreq0 23085 unisngl 23535 metrest 24537 metuel2 24578 nosupno 27748 nosupfv 27751 noinfno 27763 noinffv 27766 elold 27908 lrrecfr 27976 sleadd1 28022 addsuniflem 28034 addsasslem1 28036 addsasslem2 28037 mulsuniflem 28175 addsdilem1 28177 addsdilem2 28178 mulsasslem1 28189 mulsasslem2 28190 renegscl 28430 readdscl 28431 remulscl 28434 istrkg2ld 28468 fpwrelmapffslem 32743 omssubaddlem 34301 omssubadd 34302 bnj906 34944 satfdm 35374 dmopab3rexdif 35410 rexxfr3dALT 35644 bj-elsngl 36969 bj-restn0 37091 ismblfin 37668 itg2addnclem3 37680 sdclem1 37750 eldmqs1cossres 38660 prter2 38882 lshpsmreu 39110 islpln5 39537 islvol5 39581 cdlemftr3 40567 mapdpglem3 41677 hdmapglem7a 41929 diophrex 42786 imaiun1 43664 coiun1 43665 grumnudlem 44304 upbdrech 45317 usgrgrtrirex 47917 |
| Copyright terms: Public domain | W3C validator |