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 { 𝑧 ∈ ( 𝐴 × 𝐵 ) ∣ 𝜑 } = { 𝑥 ∈ 𝐴 ∣ ∃ 𝑦 ∈ 𝐵 𝜓 }