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

Metamath Proof Explorer

Theorem resopab

Description: Restriction of a class abstraction of ordered pairs. (Contributed by NM, 5-Nov-2002)

Ref Expression
Assertion resopab ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↾ 𝐴 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) }

Proof

Step Hyp Ref Expression
1 df-res ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↾ 𝐴 ) = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∩ ( 𝐴 × V ) )
2 df-xp ⊢ ( 𝐴 × V ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ V ) }
3 vex ⊢ 𝑦 ∈ V
4 3 biantru ⊢ ( 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ V ) )
5 4 opabbii ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ 𝐴 } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ V ) }
6 2 5 eqtr4i ⊢ ( 𝐴 × V ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ 𝐴 }
7 6 ineq2i ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∩ ( 𝐴 × V ) ) = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ 𝐴 } )
8 incom ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ 𝐴 } ) = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ 𝐴 } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } )
9 7 8 eqtri ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∩ ( 𝐴 × V ) ) = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ 𝐴 } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } )
10 inopab ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ 𝐴 } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) }
11 9 10 eqtri ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∩ ( 𝐴 × V ) ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) }
12 1 11 eqtri ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↾ 𝐴 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) }