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