![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rexv | Structured version Visualization version GIF version |
Description: An existential quantifier restricted to the universe is unrestricted. (Contributed by NM, 26-Mar-2004.) |
Ref | Expression |
---|---|
rexv | ⊢ (∃𝑥 ∈ V 𝜑 ↔ ∃𝑥𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-rex 3069 | . 2 ⊢ (∃𝑥 ∈ V 𝜑 ↔ ∃𝑥(𝑥 ∈ V ∧ 𝜑)) | |
2 | vex 3482 | . . . 4 ⊢ 𝑥 ∈ V | |
3 | 2 | biantrur 530 | . . 3 ⊢ (𝜑 ↔ (𝑥 ∈ V ∧ 𝜑)) |
4 | 3 | exbii 1845 | . 2 ⊢ (∃𝑥𝜑 ↔ ∃𝑥(𝑥 ∈ V ∧ 𝜑)) |
5 | 1, 4 | bitr4i 278 | 1 ⊢ (∃𝑥 ∈ V 𝜑 ↔ ∃𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 206 ∧ wa 395 ∃wex 1776 ∈ wcel 2106 ∃wrex 3068 Vcvv 3478 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1540 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-rex 3069 df-v 3480 |
This theorem is referenced by: spesbc 3891 exopxfr 5857 elres 6040 elid 6221 dfco2 6267 dfco2a 6268 dffv2 7004 abnex 7776 finacn 10088 ac6s2 10524 ptcmplem3 24078 ustn0 24245 hlimeui 31269 rexcom4f 32497 isrnsiga 34094 prdstotbnd 37781 ac6s3f 38158 moxfr 42680 eldioph2b 42751 kelac1 43052 cbvexsv 44545 sprid 47399 |
Copyright terms: Public domain | W3C validator |