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 3146 | . 2 ⊢ (∃𝑥 ∈ V 𝜑 ↔ ∃𝑥(𝑥 ∈ V ∧ 𝜑)) | |
2 | vex 3499 | . . . 4 ⊢ 𝑥 ∈ V | |
3 | 2 | biantrur 533 | . . 3 ⊢ (𝜑 ↔ (𝑥 ∈ V ∧ 𝜑)) |
4 | 3 | exbii 1848 | . 2 ⊢ (∃𝑥𝜑 ↔ ∃𝑥(𝑥 ∈ V ∧ 𝜑)) |
5 | 1, 4 | bitr4i 280 | 1 ⊢ (∃𝑥 ∈ V 𝜑 ↔ ∃𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 208 ∧ wa 398 ∃wex 1780 ∈ wcel 2114 ∃wrex 3141 Vcvv 3496 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-ext 2795 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1781 df-sb 2070 df-clab 2802 df-cleq 2816 df-clel 2895 df-rex 3146 df-v 3498 |
This theorem is referenced by: rexcom4OLD 3528 spesbc 3867 exopxfr 5716 elres 5893 elid 6058 dfco2 6100 dfco2a 6101 dffv2 6758 abnex 7481 finacn 9478 ac6s2 9910 ptcmplem3 22664 ustn0 22831 hlimeui 29019 rexcom4f 30236 isrnsiga 31374 prdstotbnd 35074 ac6s3f 35451 moxfr 39296 eldioph2b 39367 kelac1 39670 cbvexsv 40888 sprid 43643 |
Copyright terms: Public domain | W3C validator |