Theorem ineq1 3550

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 2504	. . . 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 3544	. . 3 |- ( x e. ( A i^i C ) <-> ( x e. A /\ x e. C ) )
4		elin 3544	. . 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 2441	1 |- ( A = B -> ( A i^i C ) = ( B i^i C ) )

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1369   e. wcel 1756   i^i cin 3332

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-v 2979  df-in 3340

This theorem is referenced by:  ineq2  3551  ineq12  3552  ineq1i  3553  ineq1d  3556  unineq  3605  dfrab3ss  3633  intprg  4167  inex1g  4440  reseq1  5109  isofrlem  6036  qsdisj  7182  fiint  7593  elfiun  7685  dffi3  7686  inf3lema  7835  dfac5lem5  8302  kmlem12  8335  kmlem14  8337  fin23lem24  8496  fin23lem26  8499  fin23lem23  8500  fin23lem22  8501  fin23lem27  8502  ingru  8987  uzin2  12837  incexclem  13304  elrestr  14372  firest  14376  inopn  18517  isbasisg  18557  basis1  18560  basis2  18561  tgval  18565  fctop  18613  cctop  18615  ntrfval  18633  elcls  18682  clsndisj  18684  elcls3  18692  neindisj2  18732  tgrest  18768  restco  18773  restsn  18779  restcld  18781  restcldi  18782  restopnb  18784  neitr  18789  restcls  18790  ordtbaslem  18797  ordtrest2lem  18812  hausnei2  18962  cnhaus  18963  regsep2  18985  dishaus  18991  ordthauslem  18992  cmpsublem  19007  cmpsub  19008  bwthOLD  19019  nconsubb  19032  consubclo  19033  1stcelcls  19070  islly  19077  cldllycmp  19104  lly1stc  19105  elkgen  19114  ptclsg  19193  dfac14lem  19195  txrest  19209  pthaus  19216  txhaus  19225  xkohaus  19231  xkoptsub  19232  regr1lem  19317  isfbas  19407  fbasssin  19414  fbun  19418  isfil  19425  fbunfip  19447  fgval  19448  filcon  19461  uzrest  19475  isufil2  19486  hauspwpwf1  19565  fclsopni  19593  fclsnei  19597  fclsrest  19602  fcfnei  19613  fcfneii  19615  tsmsfbas  19703  ustincl  19787  ustdiag  19788  ustinvel  19789  ustexhalf  19790  ust0  19799  trust  19809  restutopopn  19818  lpbl  20083  methaus  20100  metrest  20104  restmetu  20167  qtopbaslem  20342  qdensere  20354  xrtgioo  20388  metnrmlem3  20442  icoopnst  20516  iocopnst  20517  ovolicc2lem2  21006  ovolicc2lem5  21009  mblsplit  21020  limcnlp  21358  ellimc3  21359  limcflf  21361  limciun  21374  ig1pval  21649  shincl  24789  shmodi  24798  omlsi  24812  pjoml  24844  chm0  24899  chincl  24907  chdmm1  24933  ledi  24948  cmbr  24992  cmbr3  25016  mdbr  25703  dmdmd  25709  dmdi  25711  dmdbr3  25714  dmdbr4  25715  mdslmd1lem4  25737  cvmd  25745  cvexch  25783  dmdbr6ati  25832  mddmdin0i  25840  difeq  25904  ofpreima2  25990  ordtrest2NEWlem  26357  measvuni  26633  measinb  26640  totprob  26815  ballotlemgval  26911  cvmscbv  27152  cvmsdisj  27164  cvmsss2  27168  nepss  27379  sspred  27638  brapply  27974  ptrest  28430  mblfinlem2  28434  opnbnd  28525  isfne  28545  locfincmp  28581  tailfb  28603  bndss  28690  lcvexchlem4  32687