Metamath Proof Explorer

Theorem 2reu7

Description: Two equivalent expressions for double restricted existential uniqueness, analogous to 2eu7 . (Contributed by Alexander van der Vekens, 2-Jul-2017)

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

Proof

Step Hyp Ref Expression
1 nfcv ⊢Ⅎ_xB
2 nfre1 ⊢Ⅎx∃x∈Aφ
3 1 2 nfreuw ⊢Ⅎx∃!y∈B∃x∈Aφ
4 3 reuan ⊢∃!x∈A∃!y∈B∃x∈Aφ∧∃y∈Bφ↔∃!y∈B∃x∈Aφ∧∃!x∈A∃y∈Bφ
5 ancom ⊢∃x∈Aφ∧∃y∈Bφ↔∃y∈Bφ∧∃x∈Aφ
6 5 reubii ⊢∃!y∈B∃x∈Aφ∧∃y∈Bφ↔∃!y∈B∃y∈Bφ∧∃x∈Aφ
7 nfre1 ⊢Ⅎy∃y∈Bφ
8 7 reuan ⊢∃!y∈B∃y∈Bφ∧∃x∈Aφ↔∃y∈Bφ∧∃!y∈B∃x∈Aφ
9 ancom ⊢∃y∈Bφ∧∃!y∈B∃x∈Aφ↔∃!y∈B∃x∈Aφ∧∃y∈Bφ
10 6 8 9 3bitri ⊢∃!y∈B∃x∈Aφ∧∃y∈Bφ↔∃!y∈B∃x∈Aφ∧∃y∈Bφ
11 10 reubii ⊢∃!x∈A∃!y∈B∃x∈Aφ∧∃y∈Bφ↔∃!x∈A∃!y∈B∃x∈Aφ∧∃y∈Bφ
12 ancom ⊢∃!x∈A∃y∈Bφ∧∃!y∈B∃x∈Aφ↔∃!y∈B∃x∈Aφ∧∃!x∈A∃y∈Bφ
13 4 11 12 3bitr4ri ⊢∃!x∈A∃y∈Bφ∧∃!y∈B∃x∈Aφ↔∃!x∈A∃!y∈B∃x∈Aφ∧∃y∈Bφ