|   | 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 3070 | . 2 ⊢ (∃𝑥 ∈ V 𝜑 ↔ ∃𝑥(𝑥 ∈ V ∧ 𝜑)) | |
| 2 | vex 3483 | . . . 4 ⊢ 𝑥 ∈ V | |
| 3 | 2 | biantrur 530 | . . 3 ⊢ (𝜑 ↔ (𝑥 ∈ V ∧ 𝜑)) | 
| 4 | 3 | exbii 1847 | . 2 ⊢ (∃𝑥𝜑 ↔ ∃𝑥(𝑥 ∈ V ∧ 𝜑)) | 
| 5 | 1, 4 | bitr4i 278 | 1 ⊢ (∃𝑥 ∈ V 𝜑 ↔ ∃𝑥𝜑) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ↔ wb 206 ∧ wa 395 ∃wex 1778 ∈ wcel 2107 ∃wrex 3069 Vcvv 3479 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1542 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-rex 3070 df-v 3481 | 
| This theorem is referenced by: spesbc 3881 exopxfr 5853 elres 6037 elid 6218 dfco2 6264 dfco2a 6265 dffv2 7003 abnex 7778 finacn 10091 ac6s2 10527 ptcmplem3 24063 ustn0 24230 hlimeui 31260 rexcom4f 32488 isrnsiga 34115 prdstotbnd 37802 ac6s3f 38179 moxfr 42708 eldioph2b 42779 kelac1 43080 cbvexsv 44572 sprid 47466 | 
| Copyright terms: Public domain | W3C validator |