Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > rexcom4 | 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 2621 | . 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ V 𝜑 ↔ ∃𝑦 ∈ V ∃𝑥 ∈ 𝐴 𝜑) | |
2 | rexv 2730 | . . 3 ⊢ (∃𝑦 ∈ V 𝜑 ↔ ∃𝑦𝜑) | |
3 | 2 | rexbii 2464 | . 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ V 𝜑 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦𝜑) |
4 | rexv 2730 | . 2 ⊢ (∃𝑦 ∈ V ∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑) | |
5 | 1, 3, 4 | 3bitr3i 209 | 1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 ∃wex 1472 ∃wrex 2436 Vcvv 2712 |
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 1427 ax-7 1428 ax-gen 1429 ax-ie1 1473 ax-ie2 1474 ax-8 1484 ax-10 1485 ax-11 1486 ax-i12 1487 ax-bndl 1489 ax-4 1490 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2139 |
This theorem depends on definitions: df-bi 116 df-tru 1338 df-nf 1441 df-sb 1743 df-clab 2144 df-cleq 2150 df-clel 2153 df-nfc 2288 df-rex 2441 df-v 2714 |
This theorem is referenced by: rexcom4a 2736 reuind 2917 iuncom4 3858 dfiun2g 3883 iunn0m 3911 iunxiun 3932 iinexgm 4117 inuni 4118 iunopab 4243 xpiundi 4646 xpiundir 4647 cnvuni 4774 dmiun 4797 elres 4904 elsnres 4905 rniun 4998 imaco 5093 coiun 5097 fun11iun 5437 abrexco 5711 imaiun 5712 fliftf 5751 rexrnmpo 5938 oprabrexex2 6080 releldm2 6135 eroveu 6573 genpassl 7446 genpassu 7447 ltexprlemopl 7523 ltexprlemopu 7525 pceu 12185 ntreq0 12602 metrest 12976 |
Copyright terms: Public domain | W3C validator |