Theorem elv 3389

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.)

Hypothesis

Ref	Expression
elv.1	⊢ (𝑥 ∈ V → 𝜑)

Assertion

Ref	Expression
elv	⊢ 𝜑

Proof of Theorem elv

Step	Hyp	Ref	Expression
1		vex 3388	. 2 ⊢ 𝑥 ∈ V
2		elv.1	. 2 ⊢ (𝑥 ∈ V → 𝜑)
3	1, 2	ax-mp 5	1 ⊢ 𝜑

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