Theorem ineq1 3495

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 2465	. . . 4 |- ( A = B -> ( x e. A <-> x e. B ) )
2	1	anbi1d 686	. . 3 |- ( A = B -> ( ( x e. A /\ x e. C ) <-> ( x e. B /\ x e. C ) ) )
3		elin 3490	. . 3 |- ( x e. ( A i^i C ) <-> ( x e. A /\ x e. C ) )
4		elin 3490	. . 3 |- ( x e. ( B i^i C ) <-> ( x e. B /\ x e. C ) )
5	2, 3, 4	3bitr4g 280	. 2 |- ( A = B -> ( x e. ( A i^i C ) <-> x e. ( B i^i C ) ) )
6	5	eqrdv 2402	1 |- ( A = B -> ( A i^i C ) = ( B i^i C ) )

Syntax hints:   -> wi 4   /\ wa 359   = wceq 1649   e. wcel 1721   i^i cin 3279

This theorem is referenced by:  ineq2  3496  ineq12  3497  ineq1i  3498  ineq1d  3501  unineq  3551  dfrab3ss  3579  intprg  4044  inex1g  4306  reseq1  5099  isofrlem  6019  qsdisj  6940  fiint  7342  elfiun  7393  dffi3  7394  inf3lema  7535  dfac5lem5  7964  kmlem12  7997  kmlem14  7999  fin23lem24  8158  fin23lem26  8161  fin23lem23  8162  fin23lem22  8163  fin23lem27  8164  ingru  8646  uzin2  12103  incexclem  12571  elrestr  13611  firest  13615  inopn  16927  isbasisg  16967  basis1  16970  basis2  16971  tgval  16975  fctop  17023  cctop  17025  ntrfval  17043  elcls  17092  clsndisj  17094  elcls3  17102  neindisj2  17142  tgrest  17177  restco  17182  restsn  17188  restcld  17190  restcldi  17191  restopnb  17193  neitr  17198  restcls  17199  ordtbaslem  17206  ordtrest2lem  17221  hausnei2  17371  cnhaus  17372  regsep2  17394  dishaus  17400  ordthauslem  17401  cmpsublem  17416  cmpsub  17417  nconsubb  17439  consubclo  17440  1stcelcls  17477  islly  17484  cldllycmp  17511  lly1stc  17512  elkgen  17521  ptclsg  17600  dfac14lem  17602  txrest  17616  pthaus  17623  txhaus  17632  xkohaus  17638  xkoptsub  17639  regr1lem  17724  isfbas  17814  fbasssin  17821  fbun  17825  isfil  17832  fbunfip  17854  fgval  17855  filcon  17868  uzrest  17882  isufil2  17893  hauspwpwf1  17972  fclsopni  18000  fclsnei  18004  fclsrest  18009  fcfnei  18020  fcfneii  18022  tsmsfbas  18110  ustincl  18190  ustdiag  18191  ustinvel  18192  ustexhalf  18193  ust0  18202  trust  18212  restutopopn  18221  lpbl  18486  methaus  18503  metrest  18507  restmetu  18570  qtopbaslem  18745  qdensere  18757  xrtgioo  18790  metnrmlem3  18844  icoopnst  18917  iocopnst  18918  ovolicc2lem2  19367  ovolicc2lem5  19370  mblsplit  19381  limcnlp  19718  ellimc3  19719  limcflf  19721  limciun  19734  ig1pval  20048  shincl  22836  shmodi  22845  omlsi  22859  pjoml  22891  chm0  22946  chincl  22954  chdmm1  22980  ledi  22995  cmbr  23039  cmbr3  23063  mdbr  23750  dmdmd  23756  dmdi  23758  dmdbr3  23761  dmdbr4  23762  mdslmd1lem4  23784  cvmd  23792  cvexch  23830  dmdbr6ati  23879  mddmdin0i  23887  difeq  23951  measvuni  24521  measinb  24528  sibfof  24607  totprob  24638  ballotlemgval  24734  cvmscbv  24898  cvmsdisj  24910  cvmsss2  24914  nepss  25128  predeq2  25384  sspred  25388  brapply  25691  mblfinlem  26143  opnbnd  26218  isfne  26238  locfincmp  26274  tailfb  26296  bndss  26385  lcvexchlem4  29520

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-in 3287