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 ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ↾ ( 𝐴 × 𝐵 ) ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥𝐴𝑦𝐵 ) ∧ 𝜑 ) }