Metamath Proof Explorer


Theorem bj-inrab

Description: Generalization of inrab . (Contributed by BJ, 21-Apr-2019)

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

Proof

Step Hyp Ref Expression
1 an4 ( ( ( 𝑥𝐴𝜑 ) ∧ ( 𝑥𝐵𝜓 ) ) ↔ ( ( 𝑥𝐴𝑥𝐵 ) ∧ ( 𝜑𝜓 ) ) )
2 elin ( 𝑥 ∈ ( 𝐴𝐵 ) ↔ ( 𝑥𝐴𝑥𝐵 ) )
3 2 anbi1i ( ( 𝑥 ∈ ( 𝐴𝐵 ) ∧ ( 𝜑𝜓 ) ) ↔ ( ( 𝑥𝐴𝑥𝐵 ) ∧ ( 𝜑𝜓 ) ) )
4 1 3 bitr4i ( ( ( 𝑥𝐴𝜑 ) ∧ ( 𝑥𝐵𝜓 ) ) ↔ ( 𝑥 ∈ ( 𝐴𝐵 ) ∧ ( 𝜑𝜓 ) ) )
5 4 abbii { 𝑥 ∣ ( ( 𝑥𝐴𝜑 ) ∧ ( 𝑥𝐵𝜓 ) ) } = { 𝑥 ∣ ( 𝑥 ∈ ( 𝐴𝐵 ) ∧ ( 𝜑𝜓 ) ) }
6 df-rab { 𝑥𝐴𝜑 } = { 𝑥 ∣ ( 𝑥𝐴𝜑 ) }
7 df-rab { 𝑥𝐵𝜓 } = { 𝑥 ∣ ( 𝑥𝐵𝜓 ) }
8 6 7 ineq12i ( { 𝑥𝐴𝜑 } ∩ { 𝑥𝐵𝜓 } ) = ( { 𝑥 ∣ ( 𝑥𝐴𝜑 ) } ∩ { 𝑥 ∣ ( 𝑥𝐵𝜓 ) } )
9 inab ( { 𝑥 ∣ ( 𝑥𝐴𝜑 ) } ∩ { 𝑥 ∣ ( 𝑥𝐵𝜓 ) } ) = { 𝑥 ∣ ( ( 𝑥𝐴𝜑 ) ∧ ( 𝑥𝐵𝜓 ) ) }
10 8 9 eqtri ( { 𝑥𝐴𝜑 } ∩ { 𝑥𝐵𝜓 } ) = { 𝑥 ∣ ( ( 𝑥𝐴𝜑 ) ∧ ( 𝑥𝐵𝜓 ) ) }
11 df-rab { 𝑥 ∈ ( 𝐴𝐵 ) ∣ ( 𝜑𝜓 ) } = { 𝑥 ∣ ( 𝑥 ∈ ( 𝐴𝐵 ) ∧ ( 𝜑𝜓 ) ) }
12 5 10 11 3eqtr4i ( { 𝑥𝐴𝜑 } ∩ { 𝑥𝐵𝜓 } ) = { 𝑥 ∈ ( 𝐴𝐵 ) ∣ ( 𝜑𝜓 ) }