This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem resoprab

Description: Restriction of an operation class abstraction. (Contributed by NM, 10-Feb-2007)

Ref Expression
Assertion resoprab ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ↾ ( 𝐴 × 𝐵 ) ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) }

Proof

Step Hyp Ref Expression
1 resopab ⊢ ( { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) } ↾ ( 𝐴 × 𝐵 ) ) = { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) }
2 19.42vv ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) ↔ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) )
3 an12 ⊢ ( ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) ↔ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ 𝜑 ) ) )
4 eleq1 ⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) ) )
5 opelxp ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
6 4 5 bitrdi ⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) )
7 6 anbi1d ⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ 𝜑 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ) )
8 7 pm5.32i ⊢ ( ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ 𝜑 ) ) ↔ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ) )
9 3 8 bitri ⊢ ( ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) ↔ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ) )
10 9 2exbii ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ) )
11 2 10 bitr3i ⊢ ( ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ) )
12 11 opabbii ⊢ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) } = { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ) }
13 1 12 eqtri ⊢ ( { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) } ↾ ( 𝐴 × 𝐵 ) ) = { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ) }
14 dfoprab2 ⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } = { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) }
15 14 reseq1i ⊢ ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ↾ ( 𝐴 × 𝐵 ) ) = ( { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) } ↾ ( 𝐴 × 𝐵 ) )
16 dfoprab2 ⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) } = { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ) }
17 13 15 16 3eqtr4i ⊢ ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ↾ ( 𝐴 × 𝐵 ) ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) }