Theorem ineq1 3679

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 2527	. . . 4 |- ( A = B -> ( x e. A <-> x e. B ) )
2	1	anbi1d 702	. . 3 |- ( A = B -> ( ( x e. A /\ x e. C ) <-> ( x e. B /\ x e. C ) ) )
3		elin 3673	. . 3 |- ( x e. ( A i^i C ) <-> ( x e. A /\ x e. C ) )
4		elin 3673	. . 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 2451	1 |- ( A = B -> ( A i^i C ) = ( B i^i C ) )

Syntax hints:   -> wi 4   /\ wa 367   = wceq 1398   e. wcel 1823   i^i cin 3460

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-in 3468

This theorem is referenced by:  ineq2  3680  ineq12  3681  ineq1i  3682  ineq1d  3685  unineq  3745  dfrab3ss  3773  intprg  4306  inex1g  4580  reseq1  5256  isofrlem  6211  qsdisj  7380  fiint  7789  elfiun  7882  dffi3  7883  inf3lema  8032  dfac5lem5  8499  kmlem12  8532  kmlem14  8534  fin23lem24  8693  fin23lem26  8696  fin23lem23  8697  fin23lem22  8698  fin23lem27  8699  ingru  9182  uzin2  13262  incexclem  13733  elrestr  14921  firest  14925  inopn  19578  isbasisg  19618  basis1  19621  basis2  19622  tgval  19626  fctop  19675  cctop  19677  ntrfval  19695  elcls  19744  clsndisj  19746  elcls3  19754  neindisj2  19794  tgrest  19830  restco  19835  restsn  19841  restcld  19843  restcldi  19844  restopnb  19846  neitr  19851  restcls  19852  ordtbaslem  19859  ordtrest2lem  19874  hausnei2  20024  cnhaus  20025  regsep2  20047  dishaus  20053  ordthauslem  20054  cmpsublem  20069  cmpsub  20070  nconsubb  20093  consubclo  20094  1stcelcls  20131  islly  20138  cldllycmp  20165  lly1stc  20166  locfincmp  20196  elkgen  20206  ptclsg  20285  dfac14lem  20287  txrest  20301  pthaus  20308  txhaus  20317  xkohaus  20323  xkoptsub  20324  regr1lem  20409  isfbas  20499  fbasssin  20506  fbun  20510  isfil  20517  fbunfip  20539  fgval  20540  filcon  20553  uzrest  20567  isufil2  20578  hauspwpwf1  20657  fclsopni  20685  fclsnei  20689  fclsrest  20694  fcfnei  20705  fcfneii  20707  tsmsfbas  20795  ustincl  20879  ustdiag  20880  ustinvel  20881  ustexhalf  20882  ust0  20891  trust  20901  restutopopn  20910  lpbl  21175  methaus  21192  metrest  21196  restmetu  21259  qtopbaslem  21434  qdensere  21446  xrtgioo  21480  metnrmlem3  21534  icoopnst  21608  iocopnst  21609  ovolicc2lem2  22098  ovolicc2lem5  22101  mblsplit  22112  limcnlp  22451  ellimc3  22452  limcflf  22454  limciun  22467  ig1pval  22742  shincl  26500  shmodi  26509  omlsi  26523  pjoml  26555  chm0  26610  chincl  26618  chdmm1  26644  ledi  26659  cmbr  26703  cmbr3  26727  mdbr  27414  dmdmd  27420  dmdi  27422  dmdbr3  27425  dmdbr4  27426  mdslmd1lem4  27448  cvmd  27456  cvexch  27494  dmdbr6ati  27543  mddmdin0i  27551  difeq  27618  ofpreima2  27738  ordtrest2NEWlem  28142  measvuni  28425  measinb  28432  inelcarsg  28522  carsgclctunlem2  28530  totprob  28633  ballotlemgval  28729  cvmscbv  28970  cvmsdisj  28982  cvmsss2  28986  nepss  29339  sspred  29495  brapply  29819  ptrest  30291  mblfinlem2  30295  opnbnd  30386  isfne  30400  tailfb  30438  bndss  30525  islptre  31867  islpcn  31887  uzlidlring  33008  rngcvalALTV  33042  rngcval  33043  ringcvalALTV  33088  ringcval  33089  lcvexchlem4  35178  fipjust  38182