Theorem ineq2 3679

Description: Equality theorem for intersection of two classes. (Contributed by NM, 26-Dec-1993.)

Assertion

Ref	Expression
ineq2	|- ( A = B -> ( C i^i A ) = ( C i^i B ) )

Proof of Theorem ineq2

Step	Hyp	Ref	Expression
1		ineq1 3678	. 2 |- ( A = B -> ( A i^i C ) = ( B i^i C ) )
2		incom 3676	. 2 |- ( C i^i A ) = ( A i^i C )
3		incom 3676	. 2 |- ( C i^i B ) = ( B i^i C )
4	1, 2, 3	3eqtr4g 2509	1 |- ( A = B -> ( C i^i A ) = ( C i^i B ) )

Syntax hints:   -> wi 4   = wceq 1383   i^i cin 3460

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-in 3468

This theorem is referenced by:  ineq12  3680  ineq2i  3682  ineq2d  3685  uneqin  3734  intprg  4306  wefrc  4863  onfr  4907  onnseq  7017  qsdisj  7390  disjenex  7677  fiint  7799  elfiun  7892  dffi3  7893  cplem2  8311  dfac5  8512  kmlem2  8534  kmlem13  8545  kmlem14  8546  ackbij1lem16  8618  fin23lem12  8714  fin23lem19  8719  fin23lem33  8728  uzin2  13156  pgpfac1lem3  17002  pgpfac1lem5  17004  pgpfac1  17005  inopn  19281  basis1  19324  basis2  19325  baspartn  19328  fctop  19378  cctop  19380  ordtbaslem  19562  hausnei2  19727  cnhaus  19728  nrmsep  19731  isnrm2  19732  dishaus  19756  ordthauslem  19757  bwthOLD  19784  dfcon2  19793  nconsubb  19797  finlocfin  19894  dissnlocfin  19903  locfindis  19904  kgeni  19911  pthaus  20012  txhaus  20021  xkohaus  20027  regr1lem  20113  fbasssin  20210  fbun  20214  fbunfip  20243  filcon  20257  isufil2  20282  ufileu  20293  filufint  20294  fmfnfmlem4  20331  fmfnfm  20332  fclsopni  20389  fclsbas  20395  fclsrest  20398  isfcf  20408  tsmsfbas  20499  ustincl  20583  ust0  20595  metreslem  20738  methaus  20896  qtopbaslem  21138  metnrmlem3  21238  ismbl  21810  shincl  26171  chincl  26289  chdmm1  26315  ledi  26330  cmbr  26374  cmbr3i  26390  cmbr3  26398  pjoml2  26401  stcltrlem1  27067  mdbr  27085  dmdbr  27090  cvmd  27127  cvexch  27165  sumdmdii  27206  mddmdin0i  27222  ofpreima2  27380  crefeq  27721  ballotlemfval  28301  ballotlemgval  28335  cvmscbv  28576  cvmsdisj  28588  cvmsss2  28592  nepss  28968  mblfinlem2  30027  tailfb  30170  elrfi  30601  fouriersw  31903  csbresgVD  33428  lshpinN  34454  fipjust  37453  conrel1d  37464