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