Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > rexcom4 | Unicode 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 2572 | . 2 | |
2 | rexv 2678 | . . 3 | |
3 | 2 | rexbii 2419 | . 2 |
4 | rexv 2678 | . 2 | |
5 | 1, 3, 4 | 3bitr3i 209 | 1 |
Colors of variables: wff set class |
Syntax hints: wb 104 wex 1453 wrex 2394 cvv 2660 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 683 ax-5 1408 ax-7 1409 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-8 1467 ax-10 1468 ax-11 1469 ax-i12 1470 ax-bndl 1471 ax-4 1472 ax-17 1491 ax-i9 1495 ax-ial 1499 ax-i5r 1500 ax-ext 2099 |
This theorem depends on definitions: df-bi 116 df-tru 1319 df-nf 1422 df-sb 1721 df-clab 2104 df-cleq 2110 df-clel 2113 df-nfc 2247 df-rex 2399 df-v 2662 |
This theorem is referenced by: rexcom4a 2684 reuind 2862 iuncom4 3790 dfiun2g 3815 iunn0m 3843 iunxiun 3864 iinexgm 4049 inuni 4050 iunopab 4173 xpiundi 4567 xpiundir 4568 cnvuni 4695 dmiun 4718 elres 4825 elsnres 4826 rniun 4919 imaco 5014 coiun 5018 fun11iun 5356 abrexco 5628 imaiun 5629 fliftf 5668 rexrnmpo 5854 oprabrexex2 5996 releldm2 6051 eroveu 6488 genpassl 7300 genpassu 7301 ltexprlemopl 7377 ltexprlemopu 7379 ntreq0 12228 metrest 12602 |
Copyright terms: Public domain | W3C validator |