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

Metamath Proof Explorer

Theorem dfrab3ss

Description: Restricted class abstraction with a common superset. (Contributed by Stefan O'Rear, 12-Sep-2015) (Proof shortened by Mario Carneiro, 8-Nov-2015)

Ref Expression
Assertion dfrab3ss ( 𝐴 ⊆ 𝐵 → { 𝑥 ∈ 𝐴 ∣ 𝜑 } = ( 𝐴 ∩ { 𝑥 ∈ 𝐵 ∣ 𝜑 } ) )

Proof

Step Hyp Ref Expression
1 dfss2 ⊢ ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∩ 𝐵 ) = 𝐴 )
2 ineq1 ⊢ ( ( 𝐴 ∩ 𝐵 ) = 𝐴 → ( ( 𝐴 ∩ 𝐵 ) ∩ { 𝑥 ∣ 𝜑 } ) = ( 𝐴 ∩ { 𝑥 ∣ 𝜑 } ) )
3 2 eqcomd ⊢ ( ( 𝐴 ∩ 𝐵 ) = 𝐴 → ( 𝐴 ∩ { 𝑥 ∣ 𝜑 } ) = ( ( 𝐴 ∩ 𝐵 ) ∩ { 𝑥 ∣ 𝜑 } ) )
4 1 3 sylbi ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐴 ∩ { 𝑥 ∣ 𝜑 } ) = ( ( 𝐴 ∩ 𝐵 ) ∩ { 𝑥 ∣ 𝜑 } ) )
5 dfrab3 ⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = ( 𝐴 ∩ { 𝑥 ∣ 𝜑 } )
6 dfrab3 ⊢ { 𝑥 ∈ 𝐵 ∣ 𝜑 } = ( 𝐵 ∩ { 𝑥 ∣ 𝜑 } )
7 6 ineq2i ⊢ ( 𝐴 ∩ { 𝑥 ∈ 𝐵 ∣ 𝜑 } ) = ( 𝐴 ∩ ( 𝐵 ∩ { 𝑥 ∣ 𝜑 } ) )
8 inass ⊢ ( ( 𝐴 ∩ 𝐵 ) ∩ { 𝑥 ∣ 𝜑 } ) = ( 𝐴 ∩ ( 𝐵 ∩ { 𝑥 ∣ 𝜑 } ) )
9 7 8 eqtr4i ⊢ ( 𝐴 ∩ { 𝑥 ∈ 𝐵 ∣ 𝜑 } ) = ( ( 𝐴 ∩ 𝐵 ) ∩ { 𝑥 ∣ 𝜑 } )
10 4 5 9 3eqtr4g ⊢ ( 𝐴 ⊆ 𝐵 → { 𝑥 ∈ 𝐴 ∣ 𝜑 } = ( 𝐴 ∩ { 𝑥 ∈ 𝐵 ∣ 𝜑 } ) )