Metamath Proof Explorer

Theorem 2rexrsb

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

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

Proof

Step Hyp Ref Expression
1 rexrsb ⊢∃y∈Bφ↔∃w∈B∀y∈By=w→φ
2 1 rexbii ⊢∃x∈A∃y∈Bφ↔∃x∈A∃w∈B∀y∈By=w→φ
3 rexcom ⊢∃x∈A∃w∈B∀y∈By=w→φ↔∃w∈B∃x∈A∀y∈By=w→φ
4 2 3 bitri ⊢∃x∈A∃y∈Bφ↔∃w∈B∃x∈A∀y∈By=w→φ
5 rexrsb ⊢∃x∈A∀y∈By=w→φ↔∃z∈A∀x∈Ax=z→∀y∈By=w→φ
6 impexp ⊢x=z∧y=w→φ↔x=z→y=w→φ
7 6 ralbii ⊢∀y∈Bx=z∧y=w→φ↔∀y∈Bx=z→y=w→φ
8 r19.21v ⊢∀y∈Bx=z→y=w→φ↔x=z→∀y∈By=w→φ
9 7 8 bitr2i ⊢x=z→∀y∈By=w→φ↔∀y∈Bx=z∧y=w→φ
10 9 ralbii ⊢∀x∈Ax=z→∀y∈By=w→φ↔∀x∈A∀y∈Bx=z∧y=w→φ
11 10 rexbii ⊢∃z∈A∀x∈Ax=z→∀y∈By=w→φ↔∃z∈A∀x∈A∀y∈Bx=z∧y=w→φ
12 5 11 bitri ⊢∃x∈A∀y∈By=w→φ↔∃z∈A∀x∈A∀y∈Bx=z∧y=w→φ
13 12 rexbii ⊢∃w∈B∃x∈A∀y∈By=w→φ↔∃w∈B∃z∈A∀x∈A∀y∈Bx=z∧y=w→φ
14 rexcom ⊢∃w∈B∃z∈A∀x∈A∀y∈Bx=z∧y=w→φ↔∃z∈A∃w∈B∀x∈A∀y∈Bx=z∧y=w→φ
15 13 14 bitri ⊢∃w∈B∃x∈A∀y∈By=w→φ↔∃z∈A∃w∈B∀x∈A∀y∈Bx=z∧y=w→φ
16 4 15 bitri ⊢∃x∈A∃y∈Bφ↔∃z∈A∃w∈B∀x∈A∀y∈Bx=z∧y=w→φ