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 2902 | . 2 ⊢ (∃𝑥 ∈ V 𝜑 ↔ ∃𝑥(𝑥 ∈ V ∧ 𝜑)) | |
2 | vex 3176 | . . . 4 ⊢ 𝑥 ∈ V | |
3 | 2 | biantrur 526 | . . 3 ⊢ (𝜑 ↔ (𝑥 ∈ V ∧ 𝜑)) |
4 | 3 | exbii 1764 | . 2 ⊢ (∃𝑥𝜑 ↔ ∃𝑥(𝑥 ∈ V ∧ 𝜑)) |
5 | 1, 4 | bitr4i 266 | 1 ⊢ (∃𝑥 ∈ V 𝜑 ↔ ∃𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 ∧ wa 383 ∃wex 1695 ∈ wcel 1977 ∃wrex 2897 Vcvv 3173 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-12 2034 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-an 385 df-tru 1478 df-ex 1696 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-rex 2902 df-v 3175 |
This theorem is referenced by: rexcom4 3198 spesbc 3487 exopxfr 5187 dfco2 5551 dfco2a 5552 dffv2 6181 finacn 8756 ac6s2 9191 ptcmplem3 21668 ustn0 21834 hlimeui 27481 rexcom4f 28701 isrnsigaOLD 29502 isrnsiga 29503 prdstotbnd 32763 ac6s3f 33149 moxfr 36273 eldioph2b 36344 kelac1 36651 relintabex 36906 cbvexsv 37783 |
Copyright terms: Public domain | W3C validator |