Theorem inrab 4257

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 3391	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
2		df-rab 3391	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)}
3	1, 2	ineq12i 4159	. 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ 𝜓}) = ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∩ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)})
4		df-rab 3391	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓))}
5		inab 4250	. . . 4 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∩ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)}) = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝑥 ∈ 𝐴 ∧ 𝜓))}
6		anandi 677	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)))
7	6	abbii 2804	. . . 4 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓))} = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝑥 ∈ 𝐴 ∧ 𝜓))}
8	5, 7	eqtr4i 2763	. . 3 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∩ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)}) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓))}
9	4, 8	eqtr4i 2763	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)} = ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∩ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)})
10	3, 9	eqtr4i 2763	1 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)}

Syntax hints:   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {cab 2715  {crab 3390   ∩ cin 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-in 3897

This theorem is referenced by:  rabnc  4332  ixxin  13279  hashbclem  14376  phiprmpw  16704  submacs  18753  ablfacrp  20001  dfrhm2  20412  ordtbaslem  23131  ordtbas2  23134  ordtopn3  23139  ordtcld3  23142  ordthauslem  23326  pthaus  23581  xkohaus  23596  tsmsfbas  24071  minveclem3b  25373  shftmbl  25483  mumul  27131  ppiub  27155  lgsquadlem2  27332  umgrislfupgrlem  29179  numedglnl  29201  clwwlknondisj  30170  frcond3  30328  numclwwlk3lem2  30443  xppreima  32707  xpinpreima  34056  xpinpreima2  34057  measvuni  34364  subfacp1lem6  35373  satfv1  35551  cnambfre  37980  itg2addnclem2  37984  ftc1anclem6  38010  refsymrels2  38961  dfeqvrels2  38984  refrelsredund4  39028  grpods  42625  anrabdioph  43211  naddov4  43814  undisjrab  44736  smfaddlem2  47196  smfmullem4  47226