![]() |
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 3071 | . . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
3 | 2 | exbii 1851 | . . 3 ⊢ (∃𝑦∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
4 | excom 2163 | . . 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 205 ∧ wa 397 ∃wex 1782 ∈ wcel 2107 ∃wrex 3070 |
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 3071 |
This theorem is referenced by: rexcomOLD 3273 rexcom4a 3274 2ex2rexrot 3280 reuind 3712 uni0b 4895 iuncom4 4963 dfiun2g 4991 dfiun2gOLD 4992 iunn0 5028 iunxiun 5058 iinexg 5299 inuni 5301 iunopab 5517 iunopabOLD 5518 xpiundi 5703 xpiundir 5704 cnvuni 5843 dmiun 5870 dmopab2rex 5874 elsnres 5978 rniun 6101 xpdifid 6121 imaco 6204 coiun 6209 abrexco 7192 imaiun 7193 fliftf 7261 imaeqsexv 7309 imaeqexov 7593 fiun 7876 f1iun 7877 oprabrexex2 7912 releldm2 7976 oarec 8510 omeu 8533 eroveu 8754 brttrcl2 9655 dfac5lem2 10065 genpass 10950 supaddc 12127 supadd 12128 supmul1 12129 supmullem2 12131 supmul 12132 pceu 16723 4sqlem12 16833 mreiincl 17481 psgneu 19293 ntreq0 22444 unisngl 22894 metrest 23896 metuel2 23937 nosupno 27067 nosupfv 27070 noinfno 27082 noinffv 27085 elold 27221 lrrecfr 27277 sleadd1 27320 addsunif 27332 addsasslem1 27333 addsasslem2 27334 istrkg2ld 27444 fpwrelmapffslem 31696 omssubaddlem 32956 omssubadd 32957 bnj906 33599 satfdm 34020 dmopab3rexdif 34056 bj-elsngl 35485 bj-restn0 35607 ismblfin 36165 itg2addnclem3 36177 sdclem1 36248 eldmqs1cossres 37167 prter2 37389 lshpsmreu 37617 islpln5 38044 islvol5 38088 cdlemftr3 39074 mapdpglem3 40184 hdmapglem7a 40436 diophrex 41141 imaiun1 42011 coiun1 42012 grumnudlem 42653 upbdrech 43626 |
Copyright terms: Public domain | W3C validator |