Metamath Proof Explorer

Theorem inrab2

Description: Intersection with a restricted class abstraction. (Contributed by NM, 19-Nov-2007)

Ref Expression
Assertion inrab2 ${⊢}\left\{{x}\in {A}|{\phi }\right\}\cap {B}=\left\{{x}\in \left({A}\cap {B}\right)|{\phi }\right\}$

Proof

Step Hyp Ref Expression
1 df-rab ${⊢}\left\{{x}\in {A}|{\phi }\right\}=\left\{{x}|\left({x}\in {A}\wedge {\phi }\right)\right\}$
2 abid1 ${⊢}{B}=\left\{{x}|{x}\in {B}\right\}$
3 1 2 ineq12i ${⊢}\left\{{x}\in {A}|{\phi }\right\}\cap {B}=\left\{{x}|\left({x}\in {A}\wedge {\phi }\right)\right\}\cap \left\{{x}|{x}\in {B}\right\}$
4 df-rab ${⊢}\left\{{x}\in \left({A}\cap {B}\right)|{\phi }\right\}=\left\{{x}|\left({x}\in \left({A}\cap {B}\right)\wedge {\phi }\right)\right\}$
5 inab ${⊢}\left\{{x}|\left({x}\in {A}\wedge {\phi }\right)\right\}\cap \left\{{x}|{x}\in {B}\right\}=\left\{{x}|\left(\left({x}\in {A}\wedge {\phi }\right)\wedge {x}\in {B}\right)\right\}$
6 elin ${⊢}{x}\in \left({A}\cap {B}\right)↔\left({x}\in {A}\wedge {x}\in {B}\right)$
7 6 anbi1i ${⊢}\left({x}\in \left({A}\cap {B}\right)\wedge {\phi }\right)↔\left(\left({x}\in {A}\wedge {x}\in {B}\right)\wedge {\phi }\right)$
8 an32 ${⊢}\left(\left({x}\in {A}\wedge {x}\in {B}\right)\wedge {\phi }\right)↔\left(\left({x}\in {A}\wedge {\phi }\right)\wedge {x}\in {B}\right)$
9 7 8 bitri ${⊢}\left({x}\in \left({A}\cap {B}\right)\wedge {\phi }\right)↔\left(\left({x}\in {A}\wedge {\phi }\right)\wedge {x}\in {B}\right)$
10 9 abbii ${⊢}\left\{{x}|\left({x}\in \left({A}\cap {B}\right)\wedge {\phi }\right)\right\}=\left\{{x}|\left(\left({x}\in {A}\wedge {\phi }\right)\wedge {x}\in {B}\right)\right\}$
11 5 10 eqtr4i ${⊢}\left\{{x}|\left({x}\in {A}\wedge {\phi }\right)\right\}\cap \left\{{x}|{x}\in {B}\right\}=\left\{{x}|\left({x}\in \left({A}\cap {B}\right)\wedge {\phi }\right)\right\}$
12 4 11 eqtr4i ${⊢}\left\{{x}\in \left({A}\cap {B}\right)|{\phi }\right\}=\left\{{x}|\left({x}\in {A}\wedge {\phi }\right)\right\}\cap \left\{{x}|{x}\in {B}\right\}$
13 3 12 eqtr4i ${⊢}\left\{{x}\in {A}|{\phi }\right\}\cap {B}=\left\{{x}\in \left({A}\cap {B}\right)|{\phi }\right\}$