Theorem bj-inrab3

Description: Generalization of dfrab3ss , which it may shorten. (Contributed by BJ, 21-Apr-2019) (Revised by OpenAI, 7-Jul-2020)

	Ref	Expression
Assertion	bj-inrab3	⊢ ( 𝐴 ∩ { 𝑥 ∈ 𝐵 ∣ 𝜑 } ) = ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∩ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		dfrab3	⊢ { 𝑥 ∈ 𝐵 ∣ 𝜑 } = ( 𝐵 ∩ { 𝑥 ∣ 𝜑 } )
2	1	ineq2i	⊢ ( 𝐴 ∩ { 𝑥 ∈ 𝐵 ∣ 𝜑 } ) = ( 𝐴 ∩ ( 𝐵 ∩ { 𝑥 ∣ 𝜑 } ) )
3		dfrab3	⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = ( 𝐴 ∩ { 𝑥 ∣ 𝜑 } )
4	3	ineq2i	⊢ ( 𝐵 ∩ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ) = ( 𝐵 ∩ ( 𝐴 ∩ { 𝑥 ∣ 𝜑 } ) )
5		incom	⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∩ 𝐵 ) = ( 𝐵 ∩ { 𝑥 ∈ 𝐴 ∣ 𝜑 } )
6		in12	⊢ ( 𝐴 ∩ ( 𝐵 ∩ { 𝑥 ∣ 𝜑 } ) ) = ( 𝐵 ∩ ( 𝐴 ∩ { 𝑥 ∣ 𝜑 } ) )
7	4 5 6	3eqtr4i	⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∩ 𝐵 ) = ( 𝐴 ∩ ( 𝐵 ∩ { 𝑥 ∣ 𝜑 } ) )
8	2 7	eqtr4i	⊢ ( 𝐴 ∩ { 𝑥 ∈ 𝐵 ∣ 𝜑 } ) = ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∩ 𝐵 )