Metamath Proof Explorer


Theorem 19.19

Description: Theorem 19.19 of Margaris p. 90. (Contributed by NM, 12-Mar-1993)

Ref Expression
Hypothesis 19.19.1 𝑥 𝜑
Assertion 19.19 ( ∀ 𝑥 ( 𝜑𝜓 ) → ( 𝜑 ↔ ∃ 𝑥 𝜓 ) )

Proof

Step Hyp Ref Expression
1 19.19.1 𝑥 𝜑
2 1 19.9 ( ∃ 𝑥 𝜑𝜑 )
3 exbi ( ∀ 𝑥 ( 𝜑𝜓 ) → ( ∃ 𝑥 𝜑 ↔ ∃ 𝑥 𝜓 ) )
4 2 3 bitr3id ( ∀ 𝑥 ( 𝜑𝜓 ) → ( 𝜑 ↔ ∃ 𝑥 𝜓 ) )