Theorem ineq1 3693

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

Assertion

Ref	Expression
ineq1	|- ( A = B -> ( A i^i C ) = ( B i^i C ) )

Proof of Theorem ineq1

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq2 2540	. . . 4 |- ( A = B -> ( x e. A <-> x e. B ) )
2	1	anbi1d 704	. . 3 |- ( A = B -> ( ( x e. A /\ x e. C ) <-> ( x e. B /\ x e. C ) ) )
3		elin 3687	. . 3 |- ( x e. ( A i^i C ) <-> ( x e. A /\ x e. C ) )
4		elin 3687	. . 3 |- ( x e. ( B i^i C ) <-> ( x e. B /\ x e. C ) )
5	2, 3, 4	3bitr4g 288	. 2 |- ( A = B -> ( x e. ( A i^i C ) <-> x e. ( B i^i C ) ) )
6	5	eqrdv 2464	1 |- ( A = B -> ( A i^i C ) = ( B i^i C ) )

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1379   e. wcel 1767   i^i cin 3475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-in 3483

This theorem is referenced by:  ineq2  3694  ineq12  3695  ineq1i  3696  ineq1d  3699  unineq  3748  dfrab3ss  3776  intprg  4316  inex1g  4590  reseq1  5265  isofrlem  6222  qsdisj  7385  fiint  7793  elfiun  7886  dffi3  7887  inf3lema  8037  dfac5lem5  8504  kmlem12  8537  kmlem14  8539  fin23lem24  8698  fin23lem26  8701  fin23lem23  8702  fin23lem22  8703  fin23lem27  8704  ingru  9189  uzin2  13136  incexclem  13607  elrestr  14680  firest  14684  inopn  19175  isbasisg  19215  basis1  19218  basis2  19219  tgval  19223  fctop  19271  cctop  19273  ntrfval  19291  elcls  19340  clsndisj  19342  elcls3  19350  neindisj2  19390  tgrest  19426  restco  19431  restsn  19437  restcld  19439  restcldi  19440  restopnb  19442  neitr  19447  restcls  19448  ordtbaslem  19455  ordtrest2lem  19470  hausnei2  19620  cnhaus  19621  regsep2  19643  dishaus  19649  ordthauslem  19650  cmpsublem  19665  cmpsub  19666  bwthOLD  19677  nconsubb  19690  consubclo  19691  1stcelcls  19728  islly  19735  cldllycmp  19762  lly1stc  19763  elkgen  19772  ptclsg  19851  dfac14lem  19853  txrest  19867  pthaus  19874  txhaus  19883  xkohaus  19889  xkoptsub  19890  regr1lem  19975  isfbas  20065  fbasssin  20072  fbun  20076  isfil  20083  fbunfip  20105  fgval  20106  filcon  20119  uzrest  20133  isufil2  20144  hauspwpwf1  20223  fclsopni  20251  fclsnei  20255  fclsrest  20260  fcfnei  20271  fcfneii  20273  tsmsfbas  20361  ustincl  20445  ustdiag  20446  ustinvel  20447  ustexhalf  20448  ust0  20457  trust  20467  restutopopn  20476  lpbl  20741  methaus  20758  metrest  20762  restmetu  20825  qtopbaslem  21000  qdensere  21012  xrtgioo  21046  metnrmlem3  21100  icoopnst  21174  iocopnst  21175  ovolicc2lem2  21664  ovolicc2lem5  21667  mblsplit  21678  limcnlp  22017  ellimc3  22018  limcflf  22020  limciun  22033  ig1pval  22308  shincl  25975  shmodi  25984  omlsi  25998  pjoml  26030  chm0  26085  chincl  26093  chdmm1  26119  ledi  26134  cmbr  26178  cmbr3  26202  mdbr  26889  dmdmd  26895  dmdi  26897  dmdbr3  26900  dmdbr4  26901  mdslmd1lem4  26923  cvmd  26931  cvexch  26969  dmdbr6ati  27018  mddmdin0i  27026  difeq  27090  ofpreima2  27180  ordtrest2NEWlem  27540  measvuni  27825  measinb  27832  totprob  28006  ballotlemgval  28102  cvmscbv  28343  cvmsdisj  28355  cvmsss2  28359  nepss  28570  sspred  28829  brapply  29165  ptrest  29625  mblfinlem2  29629  opnbnd  29720  isfne  29740  locfincmp  29776  tailfb  29798  bndss  29885  islptre  31161  islpcn  31181  lcvexchlem4  33834  fipjust  36770