Theorem resopab2

Description: Restriction of a class abstraction of ordered pairs. (Contributed by NM, 24-Aug-2007)

	Ref	Expression
Assertion	resopab2	⊢ ( 𝐴 ⊆ 𝐵 → ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) } ↾ 𝐴 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } )

Proof

Step	Hyp	Ref	Expression
1		resopab	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) } ↾ 𝐴 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ) }
2		ssel	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )
3	2	pm4.71d	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ) )
4	3	anbi1d	⊢ ( 𝐴 ⊆ 𝐵 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝜑 ) ) )
5		anass	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝜑 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ) )
6	4 5	bitr2di	⊢ ( 𝐴 ⊆ 𝐵 → ( ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) )
7	6	opabbidv	⊢ ( 𝐴 ⊆ 𝐵 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } )
8	1 7	syl5eq	⊢ ( 𝐴 ⊆ 𝐵 → ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) } ↾ 𝐴 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } )