Theorem rmoanimALT

Description: Alternate proof of rmoanim , shorter but requiring ax-10 and ax-11 . (Contributed by Alexander van der Vekens, 25-Jun-2017) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypothesis	rmoanim.1	|- F/ x ph
Assertion	rmoanimALT	|- ( E* x e. A ( ph /\ ps ) <-> ( ph -> E* x e. A ps ) )

Proof

Step	Hyp	Ref	Expression
1		rmoanim.1	|- F/ x ph
2		impexp	|- ( ( ( ph /\ ps ) -> x = y ) <-> ( ph -> ( ps -> x = y ) ) )
3	2	ralbii	|- ( A. x e. A ( ( ph /\ ps ) -> x = y ) <-> A. x e. A ( ph -> ( ps -> x = y ) ) )
4	1	r19.21	|- ( A. x e. A ( ph -> ( ps -> x = y ) ) <-> ( ph -> A. x e. A ( ps -> x = y ) ) )
5	3 4	bitri	|- ( A. x e. A ( ( ph /\ ps ) -> x = y ) <-> ( ph -> A. x e. A ( ps -> x = y ) ) )
6	5	exbii	|- ( E. y A. x e. A ( ( ph /\ ps ) -> x = y ) <-> E. y ( ph -> A. x e. A ( ps -> x = y ) ) )
7		nfv	|- F/ y ( ph /\ ps )
8	7	rmo2	|- ( E* x e. A ( ph /\ ps ) <-> E. y A. x e. A ( ( ph /\ ps ) -> x = y ) )
9		nfv	|- F/ y ps
10	9	rmo2	|- ( E* x e. A ps <-> E. y A. x e. A ( ps -> x = y ) )
11	10	imbi2i	|- ( ( ph -> E* x e. A ps ) <-> ( ph -> E. y A. x e. A ( ps -> x = y ) ) )
12		19.37v	|- ( E. y ( ph -> A. x e. A ( ps -> x = y ) ) <-> ( ph -> E. y A. x e. A ( ps -> x = y ) ) )
13	11 12	bitr4i	|- ( ( ph -> E* x e. A ps ) <-> E. y ( ph -> A. x e. A ( ps -> x = y ) ) )
14	6 8 13	3bitr4i	|- ( E* x e. A ( ph /\ ps ) <-> ( ph -> E* x e. A ps ) )