Metamath Proof Explorer

Theorem 2reu4

Description: Definition of double restricted existential uniqueness ("exactly one x and exactly one y "), analogous to 2eu4 . (Contributed by Alexander van der Vekens, 1-Jul-2017)

Ref Expression
Assertion 2reu4 ⊢∃!x∈A∃y∈Bφ∧∃!y∈B∃x∈Aφ↔∃x∈A∃y∈Bφ∧∃z∈A∃w∈B∀x∈A∀y∈Bφ→x=z∧y=w

Proof

Step Hyp Ref Expression
1 reurex ⊢∃!x∈A∃y∈Bφ→∃x∈A∃y∈Bφ
2 rexn0 ⊢∃x∈A∃y∈Bφ→A≠∅
3 1 2 syl ⊢∃!x∈A∃y∈Bφ→A≠∅
4 reurex ⊢∃!y∈B∃x∈Aφ→∃y∈B∃x∈Aφ
5 rexn0 ⊢∃y∈B∃x∈Aφ→B≠∅
6 4 5 syl ⊢∃!y∈B∃x∈Aφ→B≠∅
7 3 6 anim12i ⊢∃!x∈A∃y∈Bφ∧∃!y∈B∃x∈Aφ→A≠∅∧B≠∅
8 ne0i ⊢x∈A→A≠∅
9 ne0i ⊢y∈B→B≠∅
10 8 9 anim12i ⊢x∈A∧y∈B→A≠∅∧B≠∅
11 10 a1d ⊢x∈A∧y∈B→φ→A≠∅∧B≠∅
12 11 rexlimivv ⊢∃x∈A∃y∈Bφ→A≠∅∧B≠∅
13 12 adantr ⊢∃x∈A∃y∈Bφ∧∃z∈A∃w∈B∀x∈A∀y∈Bφ→x=z∧y=w→A≠∅∧B≠∅
14 2reu4lem ⊢A≠∅∧B≠∅→∃!x∈A∃y∈Bφ∧∃!y∈B∃x∈Aφ↔∃x∈A∃y∈Bφ∧∃z∈A∃w∈B∀x∈A∀y∈Bφ→x=z∧y=w
15 7 13 14 pm5.21nii ⊢∃!x∈A∃y∈Bφ∧∃!y∈B∃x∈Aφ↔∃x∈A∃y∈Bφ∧∃z∈A∃w∈B∀x∈A∀y∈Bφ→x=z∧y=w