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