Metamath Proof Explorer

Theorem 2reu8

Description: Two equivalent expressions for double restricted existential uniqueness, analogous to 2eu8 . Curiously, we can put E! on either of the internal conjuncts but not both. We can also commute E! x e. A E! y e. B using 2reu7 . (Contributed by Alexander van der Vekens, 2-Jul-2017)

Ref Expression
Assertion 2reu8 ⊢∃!x∈A∃!y∈B∃x∈Aφ∧∃y∈Bφ↔∃!x∈A∃!y∈B∃!x∈Aφ∧∃y∈Bφ

Proof

Step Hyp Ref Expression
1 2reu2 ⊢∃!x∈A∃y∈Bφ→∃!y∈B∃!x∈Aφ↔∃!y∈B∃x∈Aφ
2 1 pm5.32i ⊢∃!x∈A∃y∈Bφ∧∃!y∈B∃!x∈Aφ↔∃!x∈A∃y∈Bφ∧∃!y∈B∃x∈Aφ
3 nfcv ⊢Ⅎ_xB
4 nfreu1 ⊢Ⅎx∃!x∈Aφ
5 3 4 nfreuw ⊢Ⅎx∃!y∈B∃!x∈Aφ
6 5 reuan ⊢∃!x∈A∃!y∈B∃!x∈Aφ∧∃y∈Bφ↔∃!y∈B∃!x∈Aφ∧∃!x∈A∃y∈Bφ
7 ancom ⊢∃!x∈Aφ∧∃y∈Bφ↔∃y∈Bφ∧∃!x∈Aφ
8 7 reubii ⊢∃!y∈B∃!x∈Aφ∧∃y∈Bφ↔∃!y∈B∃y∈Bφ∧∃!x∈Aφ
9 nfre1 ⊢Ⅎy∃y∈Bφ
10 9 reuan ⊢∃!y∈B∃y∈Bφ∧∃!x∈Aφ↔∃y∈Bφ∧∃!y∈B∃!x∈Aφ
11 ancom ⊢∃y∈Bφ∧∃!y∈B∃!x∈Aφ↔∃!y∈B∃!x∈Aφ∧∃y∈Bφ
12 8 10 11 3bitri ⊢∃!y∈B∃!x∈Aφ∧∃y∈Bφ↔∃!y∈B∃!x∈Aφ∧∃y∈Bφ
13 12 reubii ⊢∃!x∈A∃!y∈B∃!x∈Aφ∧∃y∈Bφ↔∃!x∈A∃!y∈B∃!x∈Aφ∧∃y∈Bφ
14 ancom ⊢∃!x∈A∃y∈Bφ∧∃!y∈B∃!x∈Aφ↔∃!y∈B∃!x∈Aφ∧∃!x∈A∃y∈Bφ
15 6 13 14 3bitr4ri ⊢∃!x∈A∃y∈Bφ∧∃!y∈B∃!x∈Aφ↔∃!x∈A∃!y∈B∃!x∈Aφ∧∃y∈Bφ
16 2reu7 ⊢∃!x∈A∃y∈Bφ∧∃!y∈B∃x∈Aφ↔∃!x∈A∃!y∈B∃x∈Aφ∧∃y∈Bφ
17 2 15 16 3bitr3ri ⊢∃!x∈A∃!y∈B∃x∈Aφ∧∃y∈Bφ↔∃!x∈A∃!y∈B∃!x∈Aφ∧∃y∈Bφ