Theorem inrab 4321

Description: Intersection of two restricted class abstractions. (Contributed by NM, 1-Sep-2006.)

Assertion

Ref	Expression
inrab	⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)}

Proof of Theorem inrab

Step	Hyp	Ref	Expression
1		df-rab 3433	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
2		df-rab 3433	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)}
3	1, 2	ineq12i 4225	. 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ 𝜓}) = ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∩ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)})
4		df-rab 3433	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓))}
5		inab 4314	. . . 4 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∩ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)}) = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝑥 ∈ 𝐴 ∧ 𝜓))}
6		anandi 676	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)))
7	6	abbii 2806	. . . 4 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓))} = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝑥 ∈ 𝐴 ∧ 𝜓))}
8	5, 7	eqtr4i 2765	. . 3 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∩ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)}) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓))}
9	4, 8	eqtr4i 2765	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)} = ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∩ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)})
10	3, 9	eqtr4i 2765	1 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)}

Syntax hints:   ∧ wa 395   = wceq 1536   ∈ wcel 2105  {cab 2711  {crab 3432   ∩ cin 3961

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-in 3969

This theorem is referenced by:  rabnc  4396  ixxin  13400  hashbclem  14487  phiprmpw  16809  submacs  18852  ablfacrp  20100  dfrhm2  20490  ordtbaslem  23211  ordtbas2  23214  ordtopn3  23219  ordtcld3  23222  ordthauslem  23406  pthaus  23661  xkohaus  23676  tsmsfbas  24151  minveclem3b  25475  shftmbl  25586  mumul  27238  ppiub  27262  lgsquadlem2  27439  umgrislfupgrlem  29153  numedglnl  29175  clwwlknondisj  30139  frcond3  30297  numclwwlk3lem2  30412  xppreima  32661  xpinpreima  33866  xpinpreima2  33867  measvuni  34194  subfacp1lem6  35169  satfv1  35347  cnambfre  37654  itg2addnclem2  37658  ftc1anclem6  37684  refsymrels2  38546  dfeqvrels2  38569  refrelsredund4  38613  grpods  42175  anrabdioph  42767  naddov4  43372  undisjrab  44301  smfaddlem2  46719  smfmullem4  46749