Theorem 19.16

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

	Ref	Expression
Hypothesis	19.16.1	$$⊢Ⅎx\phi$$
Assertion	19.16	$$⊢\forall x\left(\phi \leftrightarrow \psi \right)\to \left(\phi \leftrightarrow \forall x\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		19.16.1	$$⊢Ⅎx\phi$$
2	1	19.3	$$⊢\forall x\phi \leftrightarrow \phi$$
3		albi	$$⊢\forall x\left(\phi \leftrightarrow \psi \right)\to \left(\forall x\phi \leftrightarrow \forall x\psi \right)$$
4	2 3	bitr3id	$$⊢\forall x\left(\phi \leftrightarrow \psi \right)\to \left(\phi \leftrightarrow \forall x\psi \right)$$