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 2918 | . 2 ⊢ (∃𝑥 ∈ V 𝜑 ↔ ∃𝑥(𝑥 ∈ V ∧ 𝜑)) | |
2 | vex 3203 | . . . 4 ⊢ 𝑥 ∈ V | |
3 | 2 | biantrur 527 | . . 3 ⊢ (𝜑 ↔ (𝑥 ∈ V ∧ 𝜑)) |
4 | 3 | exbii 1774 | . 2 ⊢ (∃𝑥𝜑 ↔ ∃𝑥(𝑥 ∈ V ∧ 𝜑)) |
5 | 1, 4 | bitr4i 267 | 1 ⊢ (∃𝑥 ∈ V 𝜑 ↔ ∃𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∧ wa 384 ∃wex 1704 ∈ wcel 1990 ∃wrex 2913 Vcvv 3200 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-12 2047 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-an 386 df-tru 1486 df-ex 1705 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-rex 2918 df-v 3202 |
This theorem is referenced by: rexcom4 3225 spesbc 3521 exopxfr 5265 dfco2 5634 dfco2a 5635 dffv2 6271 abnex 6965 finacn 8873 ac6s2 9308 ptcmplem3 21858 ustn0 22024 hlimeui 28097 rexcom4f 29317 isrnsigaOLD 30175 isrnsiga 30176 prdstotbnd 33593 ac6s3f 33979 moxfr 37255 eldioph2b 37326 kelac1 37633 relintabex 37887 cbvexsv 38762 sprid 41724 |
Copyright terms: Public domain | W3C validator |