Metamath Proof Explorer

Theorem dmrab

Description: Domain of a restricted class abstraction over a cartesian product. (Contributed by Thierry Arnoux, 3-Jul-2023)

Ref Expression
Hypothesis dmrab.1 ⊢z=xy→φ↔ψ
Assertion dmrab ⊢dom⁡z∈A×B|φ=x∈A|∃y∈Bψ

Proof

Step Hyp Ref Expression
1 dmrab.1 ⊢z=xy→φ↔ψ
2 1 elrab ⊢xy∈z∈A×B|φ↔xy∈A×B∧ψ
3 opelxp ⊢xy∈A×B↔x∈A∧y∈B
4 3 anbi1i ⊢xy∈A×B∧ψ↔x∈A∧y∈B∧ψ
5 ancom ⊢x∈A∧y∈B↔y∈B∧x∈A
6 5 anbi1i ⊢x∈A∧y∈B∧ψ↔y∈B∧x∈A∧ψ
7 2 4 6 3bitri ⊢xy∈z∈A×B|φ↔y∈B∧x∈A∧ψ
8 anass ⊢y∈B∧x∈A∧ψ↔y∈B∧x∈A∧ψ
9 ancom ⊢x∈A∧ψ↔ψ∧x∈A
10 9 anbi2i ⊢y∈B∧x∈A∧ψ↔y∈B∧ψ∧x∈A
11 7 8 10 3bitri ⊢xy∈z∈A×B|φ↔y∈B∧ψ∧x∈A
12 11 exbii ⊢∃yxy∈z∈A×B|φ↔∃yy∈B∧ψ∧x∈A
13 df-rex ⊢∃y∈Bψ∧x∈A↔∃yy∈B∧ψ∧x∈A
14 r19.41v ⊢∃y∈Bψ∧x∈A↔∃y∈Bψ∧x∈A
15 12 13 14 3bitr2i ⊢∃yxy∈z∈A×B|φ↔∃y∈Bψ∧x∈A
16 15 biancomi ⊢∃yxy∈z∈A×B|φ↔x∈A∧∃y∈Bψ
17 16 abbii ⊢x|∃yxy∈z∈A×B|φ=x|x∈A∧∃y∈Bψ
18 dfdm3 ⊢dom⁡z∈A×B|φ=x|∃yxy∈z∈A×B|φ
19 df-rab ⊢x∈A|∃y∈Bψ=x|x∈A∧∃y∈Bψ
20 17 18 19 3eqtr4i ⊢dom⁡z∈A×B|φ=x∈A|∃y∈Bψ