# Metamath Proof Explorer

## Theorem resoprab2

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

Ref Expression
Assertion resoprab2 ${⊢}\left({C}\subseteq {A}\wedge {D}\subseteq {B}\right)\to {\left\{⟨⟨{x},{y}⟩,{z}⟩|\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {\phi }\right)\right\}↾}_{\left({C}×{D}\right)}=\left\{⟨⟨{x},{y}⟩,{z}⟩|\left(\left({x}\in {C}\wedge {y}\in {D}\right)\wedge {\phi }\right)\right\}$

### Proof

Step Hyp Ref Expression
1 resoprab ${⊢}{\left\{⟨⟨{x},{y}⟩,{z}⟩|\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {\phi }\right)\right\}↾}_{\left({C}×{D}\right)}=\left\{⟨⟨{x},{y}⟩,{z}⟩|\left(\left({x}\in {C}\wedge {y}\in {D}\right)\wedge \left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {\phi }\right)\right)\right\}$
2 anass ${⊢}\left(\left(\left({x}\in {C}\wedge {y}\in {D}\right)\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\right)\wedge {\phi }\right)↔\left(\left({x}\in {C}\wedge {y}\in {D}\right)\wedge \left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {\phi }\right)\right)$
3 an4 ${⊢}\left(\left({x}\in {C}\wedge {y}\in {D}\right)\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\right)↔\left(\left({x}\in {C}\wedge {x}\in {A}\right)\wedge \left({y}\in {D}\wedge {y}\in {B}\right)\right)$
4 ssel ${⊢}{C}\subseteq {A}\to \left({x}\in {C}\to {x}\in {A}\right)$
5 4 pm4.71d ${⊢}{C}\subseteq {A}\to \left({x}\in {C}↔\left({x}\in {C}\wedge {x}\in {A}\right)\right)$
6 5 bicomd ${⊢}{C}\subseteq {A}\to \left(\left({x}\in {C}\wedge {x}\in {A}\right)↔{x}\in {C}\right)$
7 ssel ${⊢}{D}\subseteq {B}\to \left({y}\in {D}\to {y}\in {B}\right)$
8 7 pm4.71d ${⊢}{D}\subseteq {B}\to \left({y}\in {D}↔\left({y}\in {D}\wedge {y}\in {B}\right)\right)$
9 8 bicomd ${⊢}{D}\subseteq {B}\to \left(\left({y}\in {D}\wedge {y}\in {B}\right)↔{y}\in {D}\right)$
10 6 9 bi2anan9 ${⊢}\left({C}\subseteq {A}\wedge {D}\subseteq {B}\right)\to \left(\left(\left({x}\in {C}\wedge {x}\in {A}\right)\wedge \left({y}\in {D}\wedge {y}\in {B}\right)\right)↔\left({x}\in {C}\wedge {y}\in {D}\right)\right)$
11 3 10 syl5bb ${⊢}\left({C}\subseteq {A}\wedge {D}\subseteq {B}\right)\to \left(\left(\left({x}\in {C}\wedge {y}\in {D}\right)\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\right)↔\left({x}\in {C}\wedge {y}\in {D}\right)\right)$
12 11 anbi1d ${⊢}\left({C}\subseteq {A}\wedge {D}\subseteq {B}\right)\to \left(\left(\left(\left({x}\in {C}\wedge {y}\in {D}\right)\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\right)\wedge {\phi }\right)↔\left(\left({x}\in {C}\wedge {y}\in {D}\right)\wedge {\phi }\right)\right)$
13 2 12 bitr3id ${⊢}\left({C}\subseteq {A}\wedge {D}\subseteq {B}\right)\to \left(\left(\left({x}\in {C}\wedge {y}\in {D}\right)\wedge \left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {\phi }\right)\right)↔\left(\left({x}\in {C}\wedge {y}\in {D}\right)\wedge {\phi }\right)\right)$
14 13 oprabbidv ${⊢}\left({C}\subseteq {A}\wedge {D}\subseteq {B}\right)\to \left\{⟨⟨{x},{y}⟩,{z}⟩|\left(\left({x}\in {C}\wedge {y}\in {D}\right)\wedge \left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {\phi }\right)\right)\right\}=\left\{⟨⟨{x},{y}⟩,{z}⟩|\left(\left({x}\in {C}\wedge {y}\in {D}\right)\wedge {\phi }\right)\right\}$
15 1 14 syl5eq ${⊢}\left({C}\subseteq {A}\wedge {D}\subseteq {B}\right)\to {\left\{⟨⟨{x},{y}⟩,{z}⟩|\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {\phi }\right)\right\}↾}_{\left({C}×{D}\right)}=\left\{⟨⟨{x},{y}⟩,{z}⟩|\left(\left({x}\in {C}\wedge {y}\in {D}\right)\wedge {\phi }\right)\right\}$