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		df-ss	⊢ ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∩ 𝐵 ) = 𝐴 )
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	⊢ ( 𝐴 ⊆ 𝐵 → { 𝑥 ∈ 𝐴 ∣ 𝜑 } = ( 𝐴 ∩ { 𝑥 ∈ 𝐵 ∣ 𝜑 } ) )