![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elv | Structured version Visualization version GIF version |
Description: If a proposition is implied by 𝑥 ∈ V (which is true, see vex 3388), then it is true. (Contributed by Peter Mazsa, 13-Oct-2018.) |
Ref | Expression |
---|---|
elv.1 | ⊢ (𝑥 ∈ V → 𝜑) |
Ref | Expression |
---|---|
elv | ⊢ 𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex 3388 | . 2 ⊢ 𝑥 ∈ V | |
2 | elv.1 | . 2 ⊢ (𝑥 ∈ V → 𝜑) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2157 Vcvv 3385 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-12 2213 ax-ext 2777 |
This theorem depends on definitions: df-bi 199 df-an 386 df-tru 1657 df-ex 1876 df-sb 2065 df-clab 2786 df-cleq 2792 df-clel 2795 df-v 3387 |
This theorem is referenced by: dfima2 5685 fpwwe2lem12 9751 ustfilxp 22344 ovoliunlem1 23610 h2hlm 28362 axhcompl-zf 28380 dfpo2 32159 dfrdg4 32571 bj-snsetex 33443 eldmres 34533 ecres 34540 ecres2 34541 eldmqsres 34548 inxprnres 34557 cnvepres 34563 idinxpss 34578 inxpssidinxp 34581 idinxpssinxp 34582 alrmomorn 34617 alrmomodm 34618 brxrn 34630 dfxrn2 34632 inxpxrn 34647 rnxrn 34650 rnxrnres 34651 rnxrncnvepres 34652 rnxrnidres 34653 1cossres 34678 dfcoels 34679 br1cossinidres 34693 br1cossincnvepres 34694 br1cossxrnidres 34695 br1cossxrncnvepres 34696 refrelcosslem 34706 coss0 34723 cossid 34724 br1cossxrncnvssrres 34752 dfrefrels2 34757 dfcnvrefrels2 34770 dfcnvrefrels3 34771 dfsymrels2 34785 dftrrels2 34815 onfrALTlem4VD 39882 eusnsn 41914 dfdfat2 41982 |
Copyright terms: Public domain | W3C validator |