Theorem ineq1 3657

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 2495	. . . 4 |- ( A = B -> ( x e. A <-> x e. B ) )
2	1	anbi1d 709	. . 3 |- ( A = B -> ( ( x e. A /\ x e. C ) <-> ( x e. B /\ x e. C ) ) )
3		elin 3649	. . 3 |- ( x e. ( A i^i C ) <-> ( x e. A /\ x e. C ) )
4		elin 3649	. . 3 |- ( x e. ( B i^i C ) <-> ( x e. B /\ x e. C ) )
5	2, 3, 4	3bitr4g 291	. 2 |- ( A = B -> ( x e. ( A i^i C ) <-> x e. ( B i^i C ) ) )
6	5	eqrdv 2419	1 |- ( A = B -> ( A i^i C ) = ( B i^i C ) )

Syntax hints:   -> wi 4   /\ wa 370   = wceq 1437   e. wcel 1868   i^i cin 3435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-v 3083  df-in 3443

This theorem is referenced by:  ineq2  3658  ineq12  3659  ineq1i  3660  ineq1d  3663  unineq  3723  dfrab3ss  3751  intprg  4287  inex1g  4564  reseq1  5115  sspred  5404  isofrlem  6243  qsdisj  7445  fiint  7851  elfiun  7947  dffi3  7948  inf3lema  8132  dfac5lem5  8559  kmlem12  8592  kmlem14  8594  fin23lem24  8753  fin23lem26  8756  fin23lem23  8757  fin23lem22  8758  fin23lem27  8759  ingru  9241  uzin2  13396  incexclem  13882  elrestr  15315  firest  15319  inopn  19916  isbasisg  19949  basis1  19952  basis2  19953  tgval  19957  fctop  20006  cctop  20008  ntrfval  20026  elcls  20076  clsndisj  20078  elcls3  20086  neindisj2  20126  tgrest  20162  restco  20167  restsn  20173  restcld  20175  restcldi  20176  restopnb  20178  neitr  20183  restcls  20184  ordtbaslem  20191  ordtrest2lem  20206  hausnei2  20356  cnhaus  20357  regsep2  20379  dishaus  20385  ordthauslem  20386  cmpsublem  20401  cmpsub  20402  nconsubb  20425  consubclo  20426  1stcelcls  20463  islly  20470  cldllycmp  20497  lly1stc  20498  locfincmp  20528  elkgen  20538  ptclsg  20617  dfac14lem  20619  txrest  20633  pthaus  20640  txhaus  20649  xkohaus  20655  xkoptsub  20656  regr1lem  20741  isfbas  20831  fbasssin  20838  fbun  20842  isfil  20849  fbunfip  20871  fgval  20872  filcon  20885  uzrest  20899  isufil2  20910  hauspwpwf1  20989  fclsopni  21017  fclsnei  21021  fclsrest  21026  fcfnei  21037  fcfneii  21039  tsmsfbas  21129  ustincl  21209  ustdiag  21210  ustinvel  21211  ustexhalf  21212  ust0  21221  trust  21231  restutopopn  21240  lpbl  21505  methaus  21522  metrest  21526  restmetu  21572  qtopbaslem  21766  qdensere  21777  xrtgioo  21811  metnrmlem3  21865  metnrmlem3OLD  21880  icoopnst  21954  iocopnst  21955  ovolicc2lem2  22458  ovolicc2lem5  22462  mblsplit  22473  limcnlp  22820  ellimc3  22821  limcflf  22823  limciun  22836  ig1pval  23111  ig1pvalOLD  23117  shincl  27020  shmodi  27029  omlsi  27043  pjoml  27075  chm0  27130  chincl  27138  chdmm1  27164  ledi  27179  cmbr  27223  cmbr3  27247  mdbr  27933  dmdmd  27939  dmdi  27941  dmdbr3  27944  dmdbr4  27945  mdslmd1lem4  27967  cvmd  27975  cvexch  28013  dmdbr6ati  28062  mddmdin0i  28070  difeq  28138  ofpreima2  28259  ordtrest2NEWlem  28724  inelsros  28996  diffiunisros  28997  measvuni  29032  measinb  29039  inelcarsg  29139  carsgclctunlem2  29147  totprob  29256  ballotlemgval  29352  ballotlemgvalOLD  29390  cvmscbv  29977  cvmsdisj  29989  cvmsss2  29993  nepss  30346  brapply  30698  opnbnd  30974  isfne  30988  tailfb  31026  ptrest  31853  poimirlem30  31884  mblfinlem2  31892  bndss  32032  lcvexchlem4  32522  fipjust  36089  islptre  37519  islpcn  37539  nnfoctbdjlem  38072  caragensplit  38100  uzlidlring  39201  rngcvalALTV  39235  rngcval  39236  ringcvalALTV  39281  ringcval  39282