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 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑𝜓 ) )
Assertion dmrab dom { 𝑧 ∈ ( 𝐴 × 𝐵 ) ∣ 𝜑 } = { 𝑥𝐴 ∣ ∃ 𝑦𝐵 𝜓 }

Proof

Step Hyp Ref Expression
1 dmrab.1 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑𝜓 ) )
2 1 elrab ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { 𝑧 ∈ ( 𝐴 × 𝐵 ) ∣ 𝜑 } ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) ∧ 𝜓 ) )
3 opelxp ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) ↔ ( 𝑥𝐴𝑦𝐵 ) )
4 3 anbi1i ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) ∧ 𝜓 ) ↔ ( ( 𝑥𝐴𝑦𝐵 ) ∧ 𝜓 ) )
5 ancom ( ( 𝑥𝐴𝑦𝐵 ) ↔ ( 𝑦𝐵𝑥𝐴 ) )
6 5 anbi1i ( ( ( 𝑥𝐴𝑦𝐵 ) ∧ 𝜓 ) ↔ ( ( 𝑦𝐵𝑥𝐴 ) ∧ 𝜓 ) )
7 2 4 6 3bitri ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { 𝑧 ∈ ( 𝐴 × 𝐵 ) ∣ 𝜑 } ↔ ( ( 𝑦𝐵𝑥𝐴 ) ∧ 𝜓 ) )
8 anass ( ( ( 𝑦𝐵𝑥𝐴 ) ∧ 𝜓 ) ↔ ( 𝑦𝐵 ∧ ( 𝑥𝐴𝜓 ) ) )
9 ancom ( ( 𝑥𝐴𝜓 ) ↔ ( 𝜓𝑥𝐴 ) )
10 9 anbi2i ( ( 𝑦𝐵 ∧ ( 𝑥𝐴𝜓 ) ) ↔ ( 𝑦𝐵 ∧ ( 𝜓𝑥𝐴 ) ) )
11 7 8 10 3bitri ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { 𝑧 ∈ ( 𝐴 × 𝐵 ) ∣ 𝜑 } ↔ ( 𝑦𝐵 ∧ ( 𝜓𝑥𝐴 ) ) )
12 11 exbii ( ∃ 𝑦𝑥 , 𝑦 ⟩ ∈ { 𝑧 ∈ ( 𝐴 × 𝐵 ) ∣ 𝜑 } ↔ ∃ 𝑦 ( 𝑦𝐵 ∧ ( 𝜓𝑥𝐴 ) ) )
13 df-rex ( ∃ 𝑦𝐵 ( 𝜓𝑥𝐴 ) ↔ ∃ 𝑦 ( 𝑦𝐵 ∧ ( 𝜓𝑥𝐴 ) ) )
14 r19.41v ( ∃ 𝑦𝐵 ( 𝜓𝑥𝐴 ) ↔ ( ∃ 𝑦𝐵 𝜓𝑥𝐴 ) )
15 12 13 14 3bitr2i ( ∃ 𝑦𝑥 , 𝑦 ⟩ ∈ { 𝑧 ∈ ( 𝐴 × 𝐵 ) ∣ 𝜑 } ↔ ( ∃ 𝑦𝐵 𝜓𝑥𝐴 ) )
16 15 biancomi ( ∃ 𝑦𝑥 , 𝑦 ⟩ ∈ { 𝑧 ∈ ( 𝐴 × 𝐵 ) ∣ 𝜑 } ↔ ( 𝑥𝐴 ∧ ∃ 𝑦𝐵 𝜓 ) )
17 16 abbii { 𝑥 ∣ ∃ 𝑦𝑥 , 𝑦 ⟩ ∈ { 𝑧 ∈ ( 𝐴 × 𝐵 ) ∣ 𝜑 } } = { 𝑥 ∣ ( 𝑥𝐴 ∧ ∃ 𝑦𝐵 𝜓 ) }
18 dfdm3 dom { 𝑧 ∈ ( 𝐴 × 𝐵 ) ∣ 𝜑 } = { 𝑥 ∣ ∃ 𝑦𝑥 , 𝑦 ⟩ ∈ { 𝑧 ∈ ( 𝐴 × 𝐵 ) ∣ 𝜑 } }
19 df-rab { 𝑥𝐴 ∣ ∃ 𝑦𝐵 𝜓 } = { 𝑥 ∣ ( 𝑥𝐴 ∧ ∃ 𝑦𝐵 𝜓 ) }
20 17 18 19 3eqtr4i dom { 𝑧 ∈ ( 𝐴 × 𝐵 ) ∣ 𝜑 } = { 𝑥𝐴 ∣ ∃ 𝑦𝐵 𝜓 }