Theorem resoprab2

Description: Restriction of an operator abstraction. (Contributed by Jeff Madsen, 2-Sep-2009)

	Ref	Expression
Assertion	resoprab2	⊢ ( ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵 ) → ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) } ↾ ( 𝐶 × 𝐷 ) ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝜑 ) } )

Proof

Step	Hyp	Ref	Expression
1		resoprab	⊢ ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) } ↾ ( 𝐶 × 𝐷 ) ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ) }
2		anass	⊢ ( ( ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝜑 ) ↔ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ) )
3		an4	⊢ ( ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ↔ ( ( 𝑥 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑦 ∈ 𝐷 ∧ 𝑦 ∈ 𝐵 ) ) )
4		ssel	⊢ ( 𝐶 ⊆ 𝐴 → ( 𝑥 ∈ 𝐶 → 𝑥 ∈ 𝐴 ) )
5	4	pm4.71d	⊢ ( 𝐶 ⊆ 𝐴 → ( 𝑥 ∈ 𝐶 ↔ ( 𝑥 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴 ) ) )
6	5	bicomd	⊢ ( 𝐶 ⊆ 𝐴 → ( ( 𝑥 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴 ) ↔ 𝑥 ∈ 𝐶 ) )
7		ssel	⊢ ( 𝐷 ⊆ 𝐵 → ( 𝑦 ∈ 𝐷 → 𝑦 ∈ 𝐵 ) )
8	7	pm4.71d	⊢ ( 𝐷 ⊆ 𝐵 → ( 𝑦 ∈ 𝐷 ↔ ( 𝑦 ∈ 𝐷 ∧ 𝑦 ∈ 𝐵 ) ) )
9	8	bicomd	⊢ ( 𝐷 ⊆ 𝐵 → ( ( 𝑦 ∈ 𝐷 ∧ 𝑦 ∈ 𝐵 ) ↔ 𝑦 ∈ 𝐷 ) )
10	6 9	bi2anan9	⊢ ( ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵 ) → ( ( ( 𝑥 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑦 ∈ 𝐷 ∧ 𝑦 ∈ 𝐵 ) ) ↔ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ) )
11	3 10	bitrid	⊢ ( ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵 ) → ( ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ↔ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ) )
12	11	anbi1d	⊢ ( ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵 ) → ( ( ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝜑 ) ↔ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝜑 ) ) )
13	2 12	bitr3id	⊢ ( ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵 ) → ( ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ) ↔ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝜑 ) ) )
14	13	oprabbidv	⊢ ( ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵 ) → { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ) } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝜑 ) } )
15	1 14	eqtrid	⊢ ( ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵 ) → ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) } ↾ ( 𝐶 × 𝐷 ) ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝜑 ) } )