Theorem inrab 3769

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 2816	. . 3
2		df-rab 2816	. . 3
3	1, 2	ineq12i 3697	. 2
4		df-rab 2816	. . 3
5		inab 3765	. . . 4
6		anandi 828	. . . . 5
7	6	abbii 2591	. . . 4
8	5, 7	eqtr4i 2489	. . 3
9	4, 8	eqtr4i 2489	. 2
10	3, 9	eqtr4i 2489	1

Syntax hints:  /\wa 369  =wceq 1395  e.wcel 1818  {cab 2442  {crab 2811  i^icin 3474

This theorem is referenced by:  rabnc  3809  ixxin  11575  hashbclem  12501  phiprmpw  14306  submacs  15996  ablfacrp  17117  dfrhm2  17366  ordtbaslem  19689  ordtbas2  19692  ordtopn3  19697  ordtcld3  19700  ordthauslem  19884  pthaus  20139  xkohaus  20154  tsmsfbas  20626  minveclem3b  21843  shftmbl  21949  mumul  23455  ppiub  23479  lgsquadlem2  23630  cusgrasizeindslem2  24474  frisusgranb  24997  numclwwlkdisj  25080  numclwwlk3lem  25108  xppreima  27487  xpinpreima  27888  xpinpreima2  27889  measvuni  28185  subfacp1lem6  28629  cnambfre  30063  itg2addnclem2  30067  ftc1anclem6  30095  anrabdioph  30714  undisjrab  31186

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-in 3482