Theorem ineq1 3675

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

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1381   e. wcel 1802   i^i cin 3457

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-v 3095  df-in 3465

This theorem is referenced by:  ineq2  3676  ineq12  3677  ineq1i  3678  ineq1d  3681  unineq  3730  dfrab3ss  3758  intprg  4302  inex1g  4576  reseq1  5253  isofrlem  6217  qsdisj  7386  fiint  7795  elfiun  7888  dffi3  7889  inf3lema  8039  dfac5lem5  8506  kmlem12  8539  kmlem14  8541  fin23lem24  8700  fin23lem26  8703  fin23lem23  8704  fin23lem22  8705  fin23lem27  8706  ingru  9191  uzin2  13151  incexclem  13622  elrestr  14698  firest  14702  inopn  19275  isbasisg  19315  basis1  19318  basis2  19319  tgval  19323  fctop  19371  cctop  19373  ntrfval  19391  elcls  19440  clsndisj  19442  elcls3  19450  neindisj2  19490  tgrest  19526  restco  19531  restsn  19537  restcld  19539  restcldi  19540  restopnb  19542  neitr  19547  restcls  19548  ordtbaslem  19555  ordtrest2lem  19570  hausnei2  19720  cnhaus  19721  regsep2  19743  dishaus  19749  ordthauslem  19750  cmpsublem  19765  cmpsub  19766  bwthOLD  19777  nconsubb  19790  consubclo  19791  1stcelcls  19828  islly  19835  cldllycmp  19862  lly1stc  19863  locfincmp  19893  elkgen  19903  ptclsg  19982  dfac14lem  19984  txrest  19998  pthaus  20005  txhaus  20014  xkohaus  20020  xkoptsub  20021  regr1lem  20106  isfbas  20196  fbasssin  20203  fbun  20207  isfil  20214  fbunfip  20236  fgval  20237  filcon  20250  uzrest  20264  isufil2  20275  hauspwpwf1  20354  fclsopni  20382  fclsnei  20386  fclsrest  20391  fcfnei  20402  fcfneii  20404  tsmsfbas  20492  ustincl  20576  ustdiag  20577  ustinvel  20578  ustexhalf  20579  ust0  20588  trust  20598  restutopopn  20607  lpbl  20872  methaus  20889  metrest  20893  restmetu  20956  qtopbaslem  21131  qdensere  21143  xrtgioo  21177  metnrmlem3  21231  icoopnst  21305  iocopnst  21306  ovolicc2lem2  21795  ovolicc2lem5  21798  mblsplit  21809  limcnlp  22148  ellimc3  22149  limcflf  22151  limciun  22164  ig1pval  22439  shincl  26164  shmodi  26173  omlsi  26187  pjoml  26219  chm0  26274  chincl  26282  chdmm1  26308  ledi  26323  cmbr  26367  cmbr3  26391  mdbr  27078  dmdmd  27084  dmdi  27086  dmdbr3  27089  dmdbr4  27090  mdslmd1lem4  27112  cvmd  27120  cvexch  27158  dmdbr6ati  27207  mddmdin0i  27215  difeq  27281  ofpreima2  27373  ordtrest2NEWlem  27770  measvuni  28051  measinb  28058  totprob  28232  ballotlemgval  28328  cvmscbv  28569  cvmsdisj  28581  cvmsss2  28585  nepss  28961  sspred  29220  brapply  29556  ptrest  30016  mblfinlem2  30020  opnbnd  30111  isfne  30125  tailfb  30163  bndss  30250  islptre  31529  islpcn  31549  uzlidlring  32435  rngcvalOLD  32488  rngcval  32489  ringcvalOLD  32528  ringcval  32529  lcvexchlem4  34464  fipjust  37415