Theorem elv 34328

Description: New way (elv 34328, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. Inference forms (with ⊢ 𝐴 ∈ V hypotheses) of the general theorems (proving ⊢ (𝐴 ∈ 𝑉 → assertions) may be superfluous. (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 3354	. 2 ⊢ 𝑥 ∈ V
2		elv.1	. 2 ⊢ (𝑥 ∈ V → 𝜑)
3	1, 2	ax-mp 5	1 ⊢ 𝜑

Syntax hints:   → wi 4   ∈ wcel 2145  Vcvv 3351

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-12 2203  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-tru 1634  df-ex 1853  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-v 3353

This theorem is referenced by:  eldmres  34379  ecres  34386  ecres2  34387  eldmqsres  34394  inxprnres  34403  cnvepres  34409  idinxpss  34426  inxpssidinxp  34429  idinxpssinxp  34430  alrmomorn  34465  alrmomodm  34466  brxrn  34478  dfxrn2  34480  inxpxrn  34495  rnxrn  34498  rnxrnres  34499  rnxrncnvepres  34500  rnxrnidres  34501  1cossres  34526  dfcoels  34527  br1cossinidres  34541  br1cossincnvepres  34542  br1cossxrnidres  34543  br1cossxrncnvepres  34544  refrelcosslem  34554  coss0  34571  cossid  34572  br1cossxrncnvssrres  34600  dfrefrels2  34605  dfcnvrefrels2  34618  dfcnvrefrels3  34619  dfsymrels2  34633