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.) |
Ref | Expression |
---|---|
rexcom4 | ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexcom 3099 | . 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ V 𝜑 ↔ ∃𝑦 ∈ V ∃𝑥 ∈ 𝐴 𝜑) | |
2 | rexv 3220 | . . 3 ⊢ (∃𝑦 ∈ V 𝜑 ↔ ∃𝑦𝜑) | |
3 | 2 | rexbii 3041 | . 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ V 𝜑 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦𝜑) |
4 | rexv 3220 | . 2 ⊢ (∃𝑦 ∈ V ∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑) | |
5 | 1, 3, 4 | 3bitr3i 290 | 1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∃wex 1704 ∃wrex 2913 Vcvv 3200 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ral 2917 df-rex 2918 df-v 3202 |
This theorem is referenced by: rexcom4a 3226 reuind 3411 uni0b 4463 iuncom4 4528 dfiun2g 4552 iunn0 4580 iunxiun 4608 iinexg 4824 inuni 4826 iunopab 5012 xpiundi 5173 xpiundir 5174 cnvuni 5309 dmiun 5333 elres 5435 elsnres 5436 rniun 5543 xpdifid 5562 imaco 5640 coiun 5645 abrexco 6502 imaiun 6503 fliftf 6565 fun11iun 7126 oprabrexex2 7158 releldm2 7218 oarec 7642 omeu 7665 eroveu 7842 dfac5lem2 8947 genpass 9831 supaddc 10990 supadd 10991 supmul1 10992 supmullem2 10994 supmul 10995 pceu 15551 4sqlem12 15660 mreiincl 16256 psgneu 17926 ntreq0 20881 unisngl 21330 metrest 22329 metuel2 22370 istrkg2ld 25359 fpwrelmapffslem 29507 omssubaddlem 30361 omssubadd 30362 bnj906 31000 nosupno 31849 nosupfv 31852 bj-elsngl 32956 bj-restn0 33043 ismblfin 33450 itg2addnclem3 33463 sdclem1 33539 prter2 34166 lshpsmreu 34396 islpln5 34821 islvol5 34865 cdlemftr3 35853 mapdpglem3 36964 hdmapglem7a 37219 diophrex 37339 imaiun1 37943 coiun1 37944 upbdrech 39519 |
Copyright terms: Public domain | W3C validator |