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-6 , ax-7 , 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	|- ( ph -> ( ps <-> ch ) )
Assertion	mobidvALT	|- ( ph -> ( E* x ps <-> E* x ch ) )

Proof

Step	Hyp	Ref	Expression
1		mobidvALT.1	|- ( ph -> ( ps <-> ch ) )
2	1	imbi1d	|- ( ph -> ( ( ps -> x = y ) <-> ( ch -> x = y ) ) )
3	2	albidv	|- ( ph -> ( A. x ( ps -> x = y ) <-> A. x ( ch -> x = y ) ) )
4	3	exbidv	|- ( ph -> ( E. y A. x ( ps -> x = y ) <-> E. y A. x ( ch -> x = y ) ) )
5		df-mo	|- ( E* x ps <-> E. y A. x ( ps -> x = y ) )
6		df-mo	|- ( E* x ch <-> E. y A. x ( ch -> x = y ) )
7	4 5 6	3bitr4g	|- ( ph -> ( E* x ps <-> E* x ch ) )