Theorem 19.9 1034

Description: A wff may be existentially quantified with a variable not free in it. Theorem 19.9 of [Margaris] p. 89. (Contributed by FL, 24-Mar-2007.)

Hypothesis

Ref	Expression
19.9.1	⊢ (φ → ∀xφ)

Assertion

Ref	Expression
19.9	⊢ (∃xφ ↔ φ)

Proof of Theorem 19.9

Step	Hyp	Ref	Expression
1		19.9t 1033	. . 3 ⊢ (∀x(φ → ∀xφ) → (∃xφ → φ))
2		19.9.1	. . 3 ⊢ (φ → ∀xφ)
3	1, 2	mpg 984	. 2 ⊢ (∃xφ → φ)
4		19.8a 1027	. 2 ⊢ (φ → ∃xφ)
5	3, 4	impbi 157	1 ⊢ (∃xφ ↔ φ)

Syntax hints:   → wi 3   ↔ wb 146  ∀wal 952  ∃wex 978

This theorem is referenced by:  excomim 1043  19.19 1053  19.23 1061  19.23ai 1062  19.36 1076  19.44 1087  19.45 1088  19.9v 1282  exists1 1455  dfid3 2834

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-4 971  ax-5o 973  ax-6o 976

This theorem depends on definitions:  df-bi 147  df-ex 979

Copyright terms: Public domain