Theorem inrab 4269

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 3397	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
2		df-rab 3397	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)}
3	1, 2	ineq12i 4171	. 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ 𝜓}) = ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∩ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)})
4		df-rab 3397	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓))}
5		inab 4262	. . . 4 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∩ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)}) = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝑥 ∈ 𝐴 ∧ 𝜓))}
6		anandi 676	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)))
7	6	abbii 2796	. . . 4 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓))} = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝑥 ∈ 𝐴 ∧ 𝜓))}
8	5, 7	eqtr4i 2755	. . 3 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∩ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)}) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓))}
9	4, 8	eqtr4i 2755	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)} = ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∩ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)})
10	3, 9	eqtr4i 2755	1 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)}

Syntax hints:   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {cab 2707  {crab 3396   ∩ cin 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-in 3912

This theorem is referenced by:  rabnc  4344  ixxin  13283  hashbclem  14377  phiprmpw  16705  submacs  18719  ablfacrp  19965  dfrhm2  20377  ordtbaslem  23091  ordtbas2  23094  ordtopn3  23099  ordtcld3  23102  ordthauslem  23286  pthaus  23541  xkohaus  23556  tsmsfbas  24031  minveclem3b  25344  shftmbl  25455  mumul  27107  ppiub  27131  lgsquadlem2  27308  umgrislfupgrlem  29085  numedglnl  29107  clwwlknondisj  30073  frcond3  30231  numclwwlk3lem2  30346  xppreima  32602  xpinpreima  33875  xpinpreima2  33876  measvuni  34183  subfacp1lem6  35160  satfv1  35338  cnambfre  37650  itg2addnclem2  37654  ftc1anclem6  37680  refsymrels2  38544  dfeqvrels2  38567  refrelsredund4  38611  grpods  42170  anrabdioph  42756  naddov4  43359  undisjrab  44282  smfaddlem2  46749  smfmullem4  46779