Theorem 19.19

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

	Ref	Expression
Hypothesis	19.19.1	$$⊢Ⅎx\phi$$
Assertion	19.19	$$⊢\forall x\left(\phi \leftrightarrow \psi \right)\to \left(\phi \leftrightarrow \exists x\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		19.19.1	$$⊢Ⅎx\phi$$
2	1	19.9	$$⊢\exists x\phi \leftrightarrow \phi$$
3		exbi	$$⊢\forall x\left(\phi \leftrightarrow \psi \right)\to \left(\exists x\phi \leftrightarrow \exists x\psi \right)$$
4	2 3	bitr3id	$$⊢\forall x\left(\phi \leftrightarrow \psi \right)\to \left(\phi \leftrightarrow \exists x\psi \right)$$