Metamath Proof Explorer


Theorem elv

Description: If a proposition is implied by x e. _V (which is true, see vex ), then it is true. (Contributed by Peter Mazsa, 13-Oct-2018)

Ref Expression
Hypothesis elv.1 x V φ
Assertion elv φ

Proof

Step Hyp Ref Expression
1 elv.1 x V φ
2 vex x V
3 2 1 ax-mp φ