This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 19.3v

Description: Version of 19.3 with a disjoint variable condition, requiring fewer axioms. Any formula can be universally quantified using a variable which it does not contain. See also 19.9v . (Contributed by Anthony Hart, 13-Sep-2011) Remove dependency on ax-7 . (Revised by Wolf Lammen, 4-Dec-2017) (Proof shortened by Wolf Lammen, 20-Oct-2023)

Ref Expression
Assertion 19.3v 
|- ( A. x ph <-> ph )

Proof

Step Hyp Ref Expression
1 spvw 
 |-  ( A. x ph -> ph )
2 ax-5 
 |-  ( ph -> A. x ph )
3 1 2 impbii 
 |-  ( A. x ph <-> ph )