Theorem 2reu5lem2

Description: Lemma for 2reu5 . (Contributed by Alexander van der Vekens, 17-Jun-2017)

	Ref	Expression
Assertion	2reu5lem2	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝜑 ↔ ∀ 𝑥 ∃* 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		df-rmo	⊢ ( ∃* 𝑦 ∈ 𝐵 𝜑 ↔ ∃* 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) )
2	1	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) )
3		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∃* 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) )
4		moanimv	⊢ ( ∃* 𝑦 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) ↔ ( 𝑥 ∈ 𝐴 → ∃* 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) )
5	4	bicomi	⊢ ( ( 𝑥 ∈ 𝐴 → ∃* 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) ↔ ∃* 𝑦 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) )
6		3anass	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) )
7	6	bicomi	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑 ) )
8	7	mobii	⊢ ( ∃* 𝑦 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) ↔ ∃* 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑 ) )
9	5 8	bitri	⊢ ( ( 𝑥 ∈ 𝐴 → ∃* 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) ↔ ∃* 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑 ) )
10	9	albii	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∃* 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) ↔ ∀ 𝑥 ∃* 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑 ) )
11	3 10	bitri	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ↔ ∀ 𝑥 ∃* 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑 ) )
12	2 11	bitri	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝜑 ↔ ∀ 𝑥 ∃* 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑 ) )