![]() |
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 2532 | . 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ V 𝜑 ↔ ∃𝑦 ∈ V ∃𝑥 ∈ 𝐴 𝜑) | |
2 | rexv 2638 | . . 3 ⊢ (∃𝑦 ∈ V 𝜑 ↔ ∃𝑦𝜑) | |
3 | 2 | rexbii 2386 | . 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ V 𝜑 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦𝜑) |
4 | rexv 2638 | . 2 ⊢ (∃𝑦 ∈ V ∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑) | |
5 | 1, 3, 4 | 3bitr3i 209 | 1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 ∃wex 1427 ∃wrex 2361 Vcvv 2620 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 666 ax-5 1382 ax-7 1383 ax-gen 1384 ax-ie1 1428 ax-ie2 1429 ax-8 1441 ax-10 1442 ax-11 1443 ax-i12 1444 ax-bndl 1445 ax-4 1446 ax-17 1465 ax-i9 1469 ax-ial 1473 ax-i5r 1474 ax-ext 2071 |
This theorem depends on definitions: df-bi 116 df-tru 1293 df-nf 1396 df-sb 1694 df-clab 2076 df-cleq 2082 df-clel 2085 df-nfc 2218 df-rex 2366 df-v 2622 |
This theorem is referenced by: rexcom4a 2644 reuind 2821 iuncom4 3743 dfiun2g 3768 iunn0m 3796 iunxiun 3816 iinexgm 3996 inuni 3997 iunopab 4117 xpiundi 4509 xpiundir 4510 cnvuni 4635 dmiun 4658 elres 4761 elsnres 4762 rniun 4855 imaco 4949 coiun 4953 fun11iun 5287 abrexco 5552 imaiun 5553 fliftf 5592 rexrnmpt2 5774 oprabrexex2 5915 releldm2 5969 eroveu 6397 genpassl 7144 genpassu 7145 ltexprlemopl 7221 ltexprlemopu 7223 ntreq0 11893 |
Copyright terms: Public domain | W3C validator |