Theorem ineq1 3533

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 2494	. . . 4 |- ( A = B -> ( x e. A <-> x e. B ) )
2	1	anbi1d 697	. . 3 |- ( A = B -> ( ( x e. A /\ x e. C ) <-> ( x e. B /\ x e. C ) ) )
3		elin 3527	. . 3 |- ( x e. ( A i^i C ) <-> ( x e. A /\ x e. C ) )
4		elin 3527	. . 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 2431	1 |- ( A = B -> ( A i^i C ) = ( B i^i C ) )

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1362   e. wcel 1755   i^i cin 3315

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-in 3323

This theorem is referenced by:  ineq2  3534  ineq12  3535  ineq1i  3536  ineq1d  3539  unineq  3588  dfrab3ss  3616  intprg  4150  inex1g  4423  reseq1  5091  isofrlem  6018  qsdisj  7165  fiint  7576  elfiun  7668  dffi3  7669  inf3lema  7818  dfac5lem5  8285  kmlem12  8318  kmlem14  8320  fin23lem24  8479  fin23lem26  8482  fin23lem23  8483  fin23lem22  8484  fin23lem27  8485  ingru  8969  uzin2  12815  incexclem  13281  elrestr  14349  firest  14353  inopn  18353  isbasisg  18393  basis1  18396  basis2  18397  tgval  18401  fctop  18449  cctop  18451  ntrfval  18469  elcls  18518  clsndisj  18520  elcls3  18528  neindisj2  18568  tgrest  18604  restco  18609  restsn  18615  restcld  18617  restcldi  18618  restopnb  18620  neitr  18625  restcls  18626  ordtbaslem  18633  ordtrest2lem  18648  hausnei2  18798  cnhaus  18799  regsep2  18821  dishaus  18827  ordthauslem  18828  cmpsublem  18843  cmpsub  18844  bwthOLD  18855  nconsubb  18868  consubclo  18869  1stcelcls  18906  islly  18913  cldllycmp  18940  lly1stc  18941  elkgen  18950  ptclsg  19029  dfac14lem  19031  txrest  19045  pthaus  19052  txhaus  19061  xkohaus  19067  xkoptsub  19068  regr1lem  19153  isfbas  19243  fbasssin  19250  fbun  19254  isfil  19261  fbunfip  19283  fgval  19284  filcon  19297  uzrest  19311  isufil2  19322  hauspwpwf1  19401  fclsopni  19429  fclsnei  19433  fclsrest  19438  fcfnei  19449  fcfneii  19451  tsmsfbas  19539  ustincl  19623  ustdiag  19624  ustinvel  19625  ustexhalf  19626  ust0  19635  trust  19645  restutopopn  19654  lpbl  19919  methaus  19936  metrest  19940  restmetu  20003  qtopbaslem  20178  qdensere  20190  xrtgioo  20224  metnrmlem3  20278  icoopnst  20352  iocopnst  20353  ovolicc2lem2  20842  ovolicc2lem5  20845  mblsplit  20856  limcnlp  21194  ellimc3  21195  limcflf  21197  limciun  21210  ig1pval  21528  shincl  24606  shmodi  24615  omlsi  24629  pjoml  24661  chm0  24716  chincl  24724  chdmm1  24750  ledi  24765  cmbr  24809  cmbr3  24833  mdbr  25520  dmdmd  25526  dmdi  25528  dmdbr3  25531  dmdbr4  25532  mdslmd1lem4  25554  cvmd  25562  cvexch  25600  dmdbr6ati  25649  mddmdin0i  25657  difeq  25722  ofpreima2  25808  ordtrest2NEWlem  26205  measvuni  26481  measinb  26488  totprob  26657  ballotlemgval  26753  cvmscbv  26994  cvmsdisj  27006  cvmsss2  27010  nepss  27220  sspred  27479  brapply  27815  ptrest  28266  mblfinlem2  28270  opnbnd  28361  isfne  28381  locfincmp  28417  tailfb  28439  bndss  28526  lcvexchlem4  32252