This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 2reu5lem1

Description: Lemma for 2reu5 . Note that E! x e. A E! y e. B ph does not mean "there is exactly one x in A and exactly one y in B such that ph holds"; see comment for 2eu5 . (Contributed by Alexander van der Vekens, 17-Jun-2017)

Ref Expression
Assertion 2reu5lem1 ( ∃! 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝜑 ↔ ∃! 𝑥 ∃! 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑 ) )

Proof

Step Hyp Ref Expression
1 df-reu ⊢ ( ∃! 𝑦 ∈ 𝐵 𝜑 ↔ ∃! 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) )
2 1 reubii ⊢ ( ∃! 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝜑 ↔ ∃! 𝑥 ∈ 𝐴 ∃! 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) )
3 df-reu ⊢ ( ∃! 𝑥 ∈ 𝐴 ∃! 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ↔ ∃! 𝑥 ( 𝑥 ∈ 𝐴 ∧ ∃! 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) )
4 euanv ⊢ ( ∃! 𝑦 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ∃! 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) )
5 4 bicomi ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ∃! 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) ↔ ∃! 𝑦 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) )
6 3anass ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) )
7 6 bicomi ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑 ) )
8 7 eubii ⊢ ( ∃! 𝑦 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) ↔ ∃! 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑 ) )
9 5 8 bitri ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ∃! 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) ↔ ∃! 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑 ) )
10 9 eubii ⊢ ( ∃! 𝑥 ( 𝑥 ∈ 𝐴 ∧ ∃! 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) ↔ ∃! 𝑥 ∃! 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑 ) )
11 3 10 bitri ⊢ ( ∃! 𝑥 ∈ 𝐴 ∃! 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ↔ ∃! 𝑥 ∃! 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑 ) )
12 2 11 bitri ⊢ ( ∃! 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝜑 ↔ ∃! 𝑥 ∃! 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑 ) )