Theorem ineq1 3692

Description: Equality theorem for intersection of two classes. (Contributed by NM, 14-Dec-1993.)

Assertion

Ref	Expression
ineq1

Proof of Theorem ineq1

Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq2 2530	. . . 4
2	1	anbi1d 704	. . 3
3		elin 3686	. . 3
4		elin 3686	. . 3
5	2, 3, 4	3bitr4g 288	. 2
6	5	eqrdv 2454	1

Syntax hints:  ->wi 4  /\wa 369  =wceq 1395  e.wcel 1818  i^icin 3474

This theorem is referenced by:  ineq2  3693  ineq12  3694  ineq1i  3695  ineq1d  3698  unineq  3747  dfrab3ss  3775  intprg  4321  inex1g  4595  reseq1  5272  isofrlem  6236  qsdisj  7407  fiint  7817  elfiun  7910  dffi3  7911  inf3lema  8062  dfac5lem5  8529  kmlem12  8562  kmlem14  8564  fin23lem24  8723  fin23lem26  8726  fin23lem23  8727  fin23lem22  8728  fin23lem27  8729  ingru  9214  uzin2  13177  incexclem  13648  elrestr  14826  firest  14830  inopn  19408  isbasisg  19448  basis1  19451  basis2  19452  tgval  19456  fctop  19505  cctop  19507  ntrfval  19525  elcls  19574  clsndisj  19576  elcls3  19584  neindisj2  19624  tgrest  19660  restco  19665  restsn  19671  restcld  19673  restcldi  19674  restopnb  19676  neitr  19681  restcls  19682  ordtbaslem  19689  ordtrest2lem  19704  hausnei2  19854  cnhaus  19855  regsep2  19877  dishaus  19883  ordthauslem  19884  cmpsublem  19899  cmpsub  19900  bwthOLD  19911  nconsubb  19924  consubclo  19925  1stcelcls  19962  islly  19969  cldllycmp  19996  lly1stc  19997  locfincmp  20027  elkgen  20037  ptclsg  20116  dfac14lem  20118  txrest  20132  pthaus  20139  txhaus  20148  xkohaus  20154  xkoptsub  20155  regr1lem  20240  isfbas  20330  fbasssin  20337  fbun  20341  isfil  20348  fbunfip  20370  fgval  20371  filcon  20384  uzrest  20398  isufil2  20409  hauspwpwf1  20488  fclsopni  20516  fclsnei  20520  fclsrest  20525  fcfnei  20536  fcfneii  20538  tsmsfbas  20626  ustincl  20710  ustdiag  20711  ustinvel  20712  ustexhalf  20713  ust0  20722  trust  20732  restutopopn  20741  lpbl  21006  methaus  21023  metrest  21027  restmetu  21090  qtopbaslem  21265  qdensere  21277  xrtgioo  21311  metnrmlem3  21365  icoopnst  21439  iocopnst  21440  ovolicc2lem2  21929  ovolicc2lem5  21932  mblsplit  21943  limcnlp  22282  ellimc3  22283  limcflf  22285  limciun  22298  ig1pval  22573  shincl  26299  shmodi  26308  omlsi  26322  pjoml  26354  chm0  26409  chincl  26417  chdmm1  26443  ledi  26458  cmbr  26502  cmbr3  26526  mdbr  27213  dmdmd  27219  dmdi  27221  dmdbr3  27224  dmdbr4  27225  mdslmd1lem4  27247  cvmd  27255  cvexch  27293  dmdbr6ati  27342  mddmdin0i  27350  difeq  27416  ofpreima2  27508  ordtrest2NEWlem  27904  measvuni  28185  measinb  28192  totprob  28366  ballotlemgval  28462  cvmscbv  28703  cvmsdisj  28715  cvmsss2  28719  nepss  29095  sspred  29252  brapply  29588  ptrest  30048  mblfinlem2  30052  opnbnd  30143  isfne  30157  tailfb  30195  bndss  30282  islptre  31625  islpcn  31645  uzlidlring  32735  rngcvalOLD  32769  rngcval  32770  ringcvalOLD  32815  ringcval  32816  lcvexchlem4  34762  fipjust  37750

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-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-v 3111  df-in 3482