Theorem 19.3r 714

Description: A wff may be quantified with a variable not free in it.

Hypothesis

Ref	Expression
19.3r.1	⊢ (φ → ∀xφ)

Assertion

Ref	Expression
19.3r	⊢ (φ ↔ ∀xφ)

Proof of Theorem 19.3r

Step	Hyp	Ref	Expression
1		19.3r.1	. 2 ⊢ (φ → ∀xφ)
2		ax-4 673	. 2 ⊢ (∀xφ → φ)
3	1, 2	impbi 139	1 ⊢ (φ ↔ ∀xφ)

Syntax hints:   → wi 2   ↔ wb 127  ∀wal 672

This theorem is referenced by:  19.16 730  19.17 731  19.27 750  19.28 751  19.37 759  eqsal 833  2eu4 1070  kmlem14 3593  zfcndrep 3760  zfcndpow 3762  zfcndac 3765

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673

This theorem depends on definitions:  df-bi 128

metamath.org