This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵 ) → ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) } ↾ ( 𝐶 × 𝐷 ) ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝜑 ) } )