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	$⊢ \forall x \in A \exists^{} y \in B φ \to (\exists^{} x \in A \exists y \in B φ \to \exists^{*} y \in B \exists x \in A φ)$

Proof

Step	Hyp	Ref	Expression
1		df-rmo	$⊢ \exists^{} y \in B φ \leftrightarrow \exists^{} y (y \in B \land φ)$
2	1	ralbii	$⊢ \forall x \in A \exists^{} y \in B φ \leftrightarrow \forall x \in A \exists^{} y (y \in B \land φ)$
3		df-ral	$⊢ \forall x \in A \exists^{} y (y \in B \land φ) \leftrightarrow \forall x (x \in A \to \exists^{} y (y \in B \land φ))$
4		moanimv	$⊢ \exists^{} y (x \in A \land (y \in B \land φ)) \leftrightarrow (x \in A \to \exists^{} y (y \in B \land φ))$
5	4	albii	$⊢ \forall x \exists^{} y (x \in A \land (y \in B \land φ)) \leftrightarrow \forall x (x \in A \to \exists^{} y (y \in B \land φ))$
6	3 5	bitr4i	$⊢ \forall x \in A \exists^{} y (y \in B \land φ) \leftrightarrow \forall x \exists^{} y (x \in A \land (y \in B \land φ))$
7		2moswapv	$⊢ \forall x \exists^{} y (x \in A \land (y \in B \land φ)) \to (\exists^{} x \exists y (x \in A \land (y \in B \land φ)) \to \exists^{*} y \exists x (x \in A \land (y \in B \land φ)))$
8		df-rmo	$⊢ \exists^{} x \in A \exists y \in B φ \leftrightarrow \exists^{} x (x \in A \land \exists y \in B φ)$
9		r19.42v	$⊢ \exists y \in B (x \in A \land φ) \leftrightarrow (x \in A \land \exists y \in B φ)$
10		df-rex	$⊢ \exists y \in B (x \in A \land φ) \leftrightarrow \exists y (y \in B \land (x \in A \land φ))$
11		an12	$⊢ (y \in B \land (x \in A \land φ)) \leftrightarrow (x \in A \land (y \in B \land φ))$
12	11	exbii	$⊢ \exists y (y \in B \land (x \in A \land φ)) \leftrightarrow \exists y (x \in A \land (y \in B \land φ))$
13	10 12	bitri	$⊢ \exists y \in B (x \in A \land φ) \leftrightarrow \exists y (x \in A \land (y \in B \land φ))$
14	9 13	bitr3i	$⊢ (x \in A \land \exists y \in B φ) \leftrightarrow \exists y (x \in A \land (y \in B \land φ))$
15	14	mobii	$⊢ \exists^{} x (x \in A \land \exists y \in B φ) \leftrightarrow \exists^{} x \exists y (x \in A \land (y \in B \land φ))$
16	8 15	bitri	$⊢ \exists^{} x \in A \exists y \in B φ \leftrightarrow \exists^{} x \exists y (x \in A \land (y \in B \land φ))$
17		df-rmo	$⊢ \exists^{} y \in B \exists x \in A φ \leftrightarrow \exists^{} y (y \in B \land \exists x \in A φ)$
18		r19.42v	$⊢ \exists x \in A (y \in B \land φ) \leftrightarrow (y \in B \land \exists x \in A φ)$
19		df-rex	$⊢ \exists x \in A (y \in B \land φ) \leftrightarrow \exists x (x \in A \land (y \in B \land φ))$
20	18 19	bitr3i	$⊢ (y \in B \land \exists x \in A φ) \leftrightarrow \exists x (x \in A \land (y \in B \land φ))$
21	20	mobii	$⊢ \exists^{} y (y \in B \land \exists x \in A φ) \leftrightarrow \exists^{} y \exists x (x \in A \land (y \in B \land φ))$
22	17 21	bitri	$⊢ \exists^{} y \in B \exists x \in A φ \leftrightarrow \exists^{} y \exists x (x \in A \land (y \in B \land φ))$
23	7 16 22	3imtr4g	$⊢ \forall x \exists^{} y (x \in A \land (y \in B \land φ)) \to (\exists^{} x \in A \exists y \in B φ \to \exists^{*} y \in B \exists x \in A φ)$
24	6 23	sylbi	$⊢ \forall x \in A \exists^{} y (y \in B \land φ) \to (\exists^{} x \in A \exists y \in B φ \to \exists^{*} y \in B \exists x \in A φ)$
25	2 24	sylbi	$⊢ \forall x \in A \exists^{} y \in B φ \to (\exists^{} x \in A \exists y \in B φ \to \exists^{*} y \in B \exists x \in A φ)$

Metamath Proof Explorer

Theorem 2rmoswap

Proof