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 2628 | . 2 | |
2 | rexv 2739 | . . 3 | |
3 | 2 | rexbii 2471 | . 2 |
4 | rexv 2739 | . 2 | |
5 | 1, 3, 4 | 3bitr3i 209 | 1 |
Colors of variables: wff set class |
Syntax hints: wb 104 wex 1479 wrex 2443 cvv 2721 |
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 699 ax-5 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-10 1492 ax-11 1493 ax-i12 1494 ax-bndl 1496 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-tru 1345 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-clel 2160 df-nfc 2295 df-rex 2448 df-v 2723 |
This theorem is referenced by: rexcom4a 2745 reuind 2926 iuncom4 3867 dfiun2g 3892 iunn0m 3920 iunxiun 3941 iinexgm 4127 inuni 4128 iunopab 4253 xpiundi 4656 xpiundir 4657 cnvuni 4784 dmiun 4807 elres 4914 elsnres 4915 rniun 5008 imaco 5103 coiun 5107 fun11iun 5447 abrexco 5721 imaiun 5722 fliftf 5761 rexrnmpo 5948 oprabrexex2 6090 releldm2 6145 eroveu 6583 genpassl 7456 genpassu 7457 ltexprlemopl 7533 ltexprlemopu 7535 pceu 12206 ntreq0 12679 metrest 13053 |
Copyright terms: Public domain | W3C validator |