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 = x y → φ ↔ ψ
Assertion dmrab ⊢ dom ⁡ z ∈ A × B | φ = x ∈ A | ∃ y ∈ B ψ

Proof

Step Hyp Ref Expression
1 dmrab.1 ⊢ z = x y → φ ↔ ψ
2 1 elrab ⊢ x y ∈ z ∈ A × B | φ ↔ x y ∈ A × B ∧ ψ
3 opelxp ⊢ x y ∈ A × B ↔ x ∈ A ∧ y ∈ B
4 3 anbi1i ⊢ x y ∈ 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 ⊢ x y ∈ 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 ⊢ x y ∈ z ∈ A × B | φ ↔ y ∈ B ∧ ψ ∧ x ∈ A
12 11 exbii ⊢ ∃ y x y ∈ z ∈ A × B | φ ↔ ∃ y y ∈ B ∧ ψ ∧ x ∈ A
13 df-rex ⊢ ∃ y ∈ B ψ ∧ x ∈ A ↔ ∃ y y ∈ B ∧ ψ ∧ x ∈ A
14 r19.41v ⊢ ∃ y ∈ B ψ ∧ x ∈ A ↔ ∃ y ∈ B ψ ∧ x ∈ A
15 12 13 14 3bitr2i ⊢ ∃ y x y ∈ z ∈ A × B | φ ↔ ∃ y ∈ B ψ ∧ x ∈ A
16 15 biancomi ⊢ ∃ y x y ∈ z ∈ A × B | φ ↔ x ∈ A ∧ ∃ y ∈ B ψ
17 16 abbii ⊢ x | ∃ y x y ∈ z ∈ A × B | φ = x | x ∈ A ∧ ∃ y ∈ B ψ
18 dfdm3 ⊢ dom ⁡ z ∈ A × B | φ = x | ∃ y x y ∈ 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 ψ