Metamath Proof Explorer

Theorem 2rexsb

Description: An equivalent expression for double restricted existence, analogous to rexsb . (Contributed by Alexander van der Vekens, 1-Jul-2017)

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

Proof

Step Hyp Ref Expression
1 rexsb ⊢∃y∈Bφ↔∃w∈B∀yy=w→φ
2 1 rexbii ⊢∃x∈A∃y∈Bφ↔∃x∈A∃w∈B∀yy=w→φ
3 rexcom ⊢∃x∈A∃w∈B∀yy=w→φ↔∃w∈B∃x∈A∀yy=w→φ
4 2 3 bitri ⊢∃x∈A∃y∈Bφ↔∃w∈B∃x∈A∀yy=w→φ
5 rexsb ⊢∃x∈A∀yy=w→φ↔∃z∈A∀xx=z→∀yy=w→φ
6 impexp ⊢x=z∧y=w→φ↔x=z→y=w→φ
7 6 albii ⊢∀yx=z∧y=w→φ↔∀yx=z→y=w→φ
8 19.21v ⊢∀yx=z→y=w→φ↔x=z→∀yy=w→φ
9 7 8 bitr2i ⊢x=z→∀yy=w→φ↔∀yx=z∧y=w→φ
10 9 albii ⊢∀xx=z→∀yy=w→φ↔∀x∀yx=z∧y=w→φ
11 10 rexbii ⊢∃z∈A∀xx=z→∀yy=w→φ↔∃z∈A∀x∀yx=z∧y=w→φ
12 5 11 bitri ⊢∃x∈A∀yy=w→φ↔∃z∈A∀x∀yx=z∧y=w→φ
13 12 rexbii ⊢∃w∈B∃x∈A∀yy=w→φ↔∃w∈B∃z∈A∀x∀yx=z∧y=w→φ
14 rexcom ⊢∃w∈B∃z∈A∀x∀yx=z∧y=w→φ↔∃z∈A∃w∈B∀x∀yx=z∧y=w→φ
15 13 14 bitri ⊢∃w∈B∃x∈A∀yy=w→φ↔∃z∈A∃w∈B∀x∀yx=z∧y=w→φ
16 4 15 bitri ⊢∃x∈A∃y∈Bφ↔∃z∈A∃w∈B∀x∀yx=z∧y=w→φ