Users' Mathboxes Mathbox for Peter Mazsa < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  elv Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 vex 3354 . 2 𝑥 ∈ V
2 elv.1 . 2 (𝑥 ∈ V → 𝜑)
31, 2ax-mp 5 1 𝜑
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator