Theorem ineq1 3638

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 2528	. . . 4 |- ( A = B -> ( x e. A <-> x e. B ) )
2	1	anbi1d 716	. . 3 |- ( A = B -> ( ( x e. A /\ x e. C ) <-> ( x e. B /\ x e. C ) ) )
3		elin 3628	. . 3 |- ( x e. ( A i^i C ) <-> ( x e. A /\ x e. C ) )
4		elin 3628	. . 3 |- ( x e. ( B i^i C ) <-> ( x e. B /\ x e. C ) )
5	2, 3, 4	3bitr4g 296	. 2 |- ( A = B -> ( x e. ( A i^i C ) <-> x e. ( B i^i C ) ) )
6	5	eqrdv 2459	1 |- ( A = B -> ( A i^i C ) = ( B i^i C ) )

Syntax hints:   -> wi 4   /\ wa 375   = wceq 1454   e. wcel 1897   i^i cin 3414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-v 3058  df-in 3422

This theorem is referenced by:  ineq2  3639  ineq12  3640  ineq1i  3641  ineq1d  3644  unineq  3704  dfrab3ss  3732  intprg  4282  inex1g  4559  reseq1  5117  sspred  5406  isofrlem  6255  qsdisj  7465  fiint  7873  elfiun  7969  dffi3  7970  inf3lema  8154  dfac5lem5  8583  kmlem12  8616  kmlem14  8618  fin23lem24  8777  fin23lem26  8780  fin23lem23  8781  fin23lem22  8782  fin23lem27  8783  ingru  9265  uzin2  13455  incexclem  13942  elrestr  15375  firest  15379  inopn  19977  isbasisg  20010  basis1  20013  basis2  20014  tgval  20018  fctop  20067  cctop  20069  ntrfval  20087  elcls  20137  clsndisj  20139  elcls3  20147  neindisj2  20187  tgrest  20223  restco  20228  restsn  20234  restcld  20236  restcldi  20237  restopnb  20239  neitr  20244  restcls  20245  ordtbaslem  20252  ordtrest2lem  20267  hausnei2  20417  cnhaus  20418  regsep2  20440  dishaus  20446  ordthauslem  20447  cmpsublem  20462  cmpsub  20463  nconsubb  20486  consubclo  20487  1stcelcls  20524  islly  20531  cldllycmp  20558  lly1stc  20559  locfincmp  20589  elkgen  20599  ptclsg  20678  dfac14lem  20680  txrest  20694  pthaus  20701  txhaus  20710  xkohaus  20716  xkoptsub  20717  regr1lem  20802  isfbas  20892  fbasssin  20899  fbun  20903  isfil  20910  fbunfip  20932  fgval  20933  filcon  20946  uzrest  20960  isufil2  20971  hauspwpwf1  21050  fclsopni  21078  fclsnei  21082  fclsrest  21087  fcfnei  21098  fcfneii  21100  tsmsfbas  21190  ustincl  21270  ustdiag  21271  ustinvel  21272  ustexhalf  21273  ust0  21282  trust  21292  restutopopn  21301  lpbl  21566  methaus  21583  metrest  21587  restmetu  21633  qtopbaslem  21827  qdensere  21838  xrtgioo  21872  metnrmlem3  21926  metnrmlem3OLD  21941  icoopnst  22015  iocopnst  22016  ovolicc2lem2  22519  ovolicc2lem5  22523  mblsplit  22534  limcnlp  22881  ellimc3  22882  limcflf  22884  limciun  22897  ig1pval  23172  ig1pvalOLD  23178  shincl  27082  shmodi  27091  omlsi  27105  pjoml  27137  chm0  27192  chincl  27200  chdmm1  27226  ledi  27241  cmbr  27285  cmbr3  27309  mdbr  27995  dmdmd  28001  dmdi  28003  dmdbr3  28006  dmdbr4  28007  mdslmd1lem4  28029  cvmd  28037  cvexch  28075  dmdbr6ati  28124  mddmdin0i  28132  difeq  28199  ofpreima2  28317  ordtrest2NEWlem  28776  inelsros  29048  diffiunisros  29049  measvuni  29084  measinb  29091  inelcarsg  29191  carsgclctunlem2  29199  totprob  29308  ballotlemgval  29404  ballotlemgvalOLD  29442  cvmscbv  30029  cvmsdisj  30041  cvmsss2  30045  nepss  30398  brapply  30753  opnbnd  31029  isfne  31043  tailfb  31081  ptrest  31983  poimirlem30  32014  mblfinlem2  32022  bndss  32162  lcvexchlem4  32647  fipjust  36213  islptre  37736  islpcn  37756  nnfoctbdjlem  38330  caragensplit  38358  uzlidlring  40201  rngcvalALTV  40235  rngcval  40236  ringcvalALTV  40281  ringcval  40282