Theorem inrab2 4263

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

Assertion

Ref	Expression
inrab2	⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ 𝐵) = {𝑥 ∈ (𝐴 ∩ 𝐵) ∣ 𝜑}

Distinct variable group:   𝑥,𝐵

Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑥)

Proof of Theorem inrab2

Step	Hyp	Ref	Expression
1		df-rab 3413	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
2		abid1 2896	. . 3 ⊢ 𝐵 = {𝑥 ∣ 𝑥 ∈ 𝐵}
3	1, 2	ineq12i 4164	. 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ 𝐵) = ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∩ {𝑥 ∣ 𝑥 ∈ 𝐵})
4		df-rab 3413	. . 3 ⊢ {𝑥 ∈ (𝐴 ∩ 𝐵) ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ (𝐴 ∩ 𝐵) ∧ 𝜑)}
5		inab 4255	. . . 4 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∩ {𝑥 ∣ 𝑥 ∈ 𝐵}) = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝑥 ∈ 𝐵)}
6		elin 3915	. . . . . . 7 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
7	6	anbi1i 636	. . . . . 6 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ∧ 𝜑) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∧ 𝜑))
8		an32 659	. . . . . 6 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∧ 𝜑) ↔ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝑥 ∈ 𝐵))
9	7, 8	bitri 278	. . . . 5 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ∧ 𝜑) ↔ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝑥 ∈ 𝐵))
10	9	abbii 2827	. . . 4 ⊢ {𝑥 ∣ (𝑥 ∈ (𝐴 ∩ 𝐵) ∧ 𝜑)} = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝑥 ∈ 𝐵)}
11	5, 10	eqtr4i 2786	. . 3 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∩ {𝑥 ∣ 𝑥 ∈ 𝐵}) = {𝑥 ∣ (𝑥 ∈ (𝐴 ∩ 𝐵) ∧ 𝜑)}
12	4, 11	eqtr4i 2786	. 2 ⊢ {𝑥 ∈ (𝐴 ∩ 𝐵) ∣ 𝜑} = ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∩ {𝑥 ∣ 𝑥 ∈ 𝐵})
13	3, 12	eqtr4i 2786	1 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ 𝐵) = {𝑥 ∈ (𝐴 ∩ 𝐵) ∣ 𝜑}

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570   ∈ wcel 2145  {cab 2738  {crab 3412   ∩ cin 3898

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-in 3906

This theorem is used by:  iooval2  13431  fzval2  13564  smuval2  16572  smueqlem  16580  dfphi2  16865  ordtrest  23427  ordtrest2lem  23428  rspectopn  34377  ordtrestNEW  34431  ordtrest2NEWlem  34432  itg2addnclem2  38421  isubgr0uhgr  48789  dmatALTbas  49331