Theorem mobidvALT

Description: Alternate proof of mobidv directly from its analogues albidv and exbidv , using deduction style. Note the proof structure, similar to mobi . (Contributed by Mario Carneiro, 7-Oct-2016) Reduce axiom dependencies and shorten proof. Remove dependency on ax-12 by adapting proof of mobid . (Revised by BJ, 26-Sep-2022) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	mobidvALT.1	$$⊢\phi \to \left(\psi \leftrightarrow \chi \right)$$
Assertion	mobidvALT	$$⊢\phi \to \left({\exists }^{*}x\psi \leftrightarrow {\exists }^{*}x\chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		mobidvALT.1	$$⊢\phi \to \left(\psi \leftrightarrow \chi \right)$$
2	1	imbi1d	$$⊢\phi \to \left(\left(\psi \to x=y\right)\leftrightarrow \left(\chi \to x=y\right)\right)$$
3	2	albidv	$$⊢\phi \to \left(\forall x\left(\psi \to x=y\right)\leftrightarrow \forall x\left(\chi \to x=y\right)\right)$$
4	3	exbidv	$$⊢\phi \to \left(\exists y\forall x\left(\psi \to x=y\right)\leftrightarrow \exists y\forall x\left(\chi \to x=y\right)\right)$$
5		dfmo	$$⊢{\exists }^{*}x\psi \leftrightarrow \exists y\forall x\left(\psi \to x=y\right)$$
6		dfmo	$$⊢{\exists }^{*}x\chi \leftrightarrow \exists y\forall x\left(\chi \to x=y\right)$$
7	4 5 6	3bitr4g	$$⊢\phi \to \left({\exists }^{*}x\psi \leftrightarrow {\exists }^{*}x\chi \right)$$