Theorem 2rmoswap

Description: A condition allowing to swap restricted "at most one" and restricted existential quantifiers, analogous to 2moswap . (Contributed by Alexander van der Vekens, 25-Jun-2017)

	Ref	Expression
Assertion	2rmoswap	|- ( A. x e. A E* y e. B ph -> ( E* x e. A E. y e. B ph -> E* y e. B E. x e. A ph ) )

Proof

Step	Hyp	Ref	Expression
1		df-rmo	|- ( E* y e. B ph <-> E* y ( y e. B /\ ph ) )
2	1	ralbii	|- ( A. x e. A E* y e. B ph <-> A. x e. A E* y ( y e. B /\ ph ) )
3		df-ral	|- ( A. x e. A E* y ( y e. B /\ ph ) <-> A. x ( x e. A -> E* y ( y e. B /\ ph ) ) )
4		moanimv	|- ( E* y ( x e. A /\ ( y e. B /\ ph ) ) <-> ( x e. A -> E* y ( y e. B /\ ph ) ) )
5	4	albii	|- ( A. x E* y ( x e. A /\ ( y e. B /\ ph ) ) <-> A. x ( x e. A -> E* y ( y e. B /\ ph ) ) )
6	3 5	bitr4i	|- ( A. x e. A E* y ( y e. B /\ ph ) <-> A. x E* y ( x e. A /\ ( y e. B /\ ph ) ) )
7		2moswapv	|- ( A. x E* y ( x e. A /\ ( y e. B /\ ph ) ) -> ( E* x E. y ( x e. A /\ ( y e. B /\ ph ) ) -> E* y E. x ( x e. A /\ ( y e. B /\ ph ) ) ) )
8		df-rmo	|- ( E* x e. A E. y e. B ph <-> E* x ( x e. A /\ E. y e. B ph ) )
9		r19.42v	|- ( E. y e. B ( x e. A /\ ph ) <-> ( x e. A /\ E. y e. B ph ) )
10		df-rex	|- ( E. y e. B ( x e. A /\ ph ) <-> E. y ( y e. B /\ ( x e. A /\ ph ) ) )
11		an12	|- ( ( y e. B /\ ( x e. A /\ ph ) ) <-> ( x e. A /\ ( y e. B /\ ph ) ) )
12	11	exbii	|- ( E. y ( y e. B /\ ( x e. A /\ ph ) ) <-> E. y ( x e. A /\ ( y e. B /\ ph ) ) )
13	10 12	bitri	|- ( E. y e. B ( x e. A /\ ph ) <-> E. y ( x e. A /\ ( y e. B /\ ph ) ) )
14	9 13	bitr3i	|- ( ( x e. A /\ E. y e. B ph ) <-> E. y ( x e. A /\ ( y e. B /\ ph ) ) )
15	14	mobii	|- ( E* x ( x e. A /\ E. y e. B ph ) <-> E* x E. y ( x e. A /\ ( y e. B /\ ph ) ) )
16	8 15	bitri	|- ( E* x e. A E. y e. B ph <-> E* x E. y ( x e. A /\ ( y e. B /\ ph ) ) )
17		df-rmo	|- ( E* y e. B E. x e. A ph <-> E* y ( y e. B /\ E. x e. A ph ) )
18		r19.42v	|- ( E. x e. A ( y e. B /\ ph ) <-> ( y e. B /\ E. x e. A ph ) )
19		df-rex	|- ( E. x e. A ( y e. B /\ ph ) <-> E. x ( x e. A /\ ( y e. B /\ ph ) ) )
20	18 19	bitr3i	|- ( ( y e. B /\ E. x e. A ph ) <-> E. x ( x e. A /\ ( y e. B /\ ph ) ) )
21	20	mobii	|- ( E* y ( y e. B /\ E. x e. A ph ) <-> E* y E. x ( x e. A /\ ( y e. B /\ ph ) ) )
22	17 21	bitri	|- ( E* y e. B E. x e. A ph <-> E* y E. x ( x e. A /\ ( y e. B /\ ph ) ) )
23	7 16 22	3imtr4g	|- ( A. x E* y ( x e. A /\ ( y e. B /\ ph ) ) -> ( E* x e. A E. y e. B ph -> E* y e. B E. x e. A ph ) )
24	6 23	sylbi	|- ( A. x e. A E* y ( y e. B /\ ph ) -> ( E* x e. A E. y e. B ph -> E* y e. B E. x e. A ph ) )
25	2 24	sylbi	|- ( A. x e. A E* y e. B ph -> ( E* x e. A E. y e. B ph -> E* y e. B E. x e. A ph ) )