Theorem ineq2 3601

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 3600	. 2 |- ( A = B -> ( A i^i C ) = ( B i^i C ) )
2		incom 3598	. 2 |- ( C i^i A ) = ( A i^i C )
3		incom 3598	. 2 |- ( C i^i B ) = ( B i^i C )
4	1, 2, 3	3eqtr4g 2487	1 |- ( A = B -> ( C i^i A ) = ( C i^i B ) )

Syntax hints:   -> wi 4   = wceq 1437   i^i cin 3378

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-v 3024  df-in 3386

This theorem is referenced by:  ineq12  3602  ineq2i  3604  ineq2d  3607  uneqin  3667  intprg  4233  wefrc  4790  onfr  5424  onnseq  7018  qsdisj  7395  disjenex  7683  fiint  7801  elfiun  7897  dffi3  7898  cplem2  8313  dfac5  8510  kmlem2  8532  kmlem13  8543  kmlem14  8544  ackbij1lem16  8616  fin23lem12  8712  fin23lem19  8717  fin23lem33  8726  uzin2  13351  pgpfac1lem3  17653  pgpfac1lem5  17655  pgpfac1  17656  inopn  19871  basis1  19907  basis2  19908  baspartn  19911  fctop  19961  cctop  19963  ordtbaslem  20146  hausnei2  20311  cnhaus  20312  nrmsep  20315  isnrm2  20316  dishaus  20340  ordthauslem  20341  dfcon2  20376  nconsubb  20380  finlocfin  20477  dissnlocfin  20486  locfindis  20487  kgeni  20494  pthaus  20595  txhaus  20604  xkohaus  20610  regr1lem  20696  fbasssin  20793  fbun  20797  fbunfip  20826  filcon  20840  isufil2  20865  ufileu  20876  filufint  20877  fmfnfmlem4  20914  fmfnfm  20915  fclsopni  20972  fclsbas  20978  fclsrest  20981  isfcf  20991  tsmsfbas  21084  ustincl  21164  ust0  21176  metreslem  21319  methaus  21477  qtopbaslem  21721  metnrmlem3  21820  metnrmlem3OLD  21835  ismbl  22422  shincl  26976  chincl  27094  chdmm1  27120  ledi  27135  cmbr  27179  cmbr3i  27195  cmbr3  27203  pjoml2  27206  stcltrlem1  27871  mdbr  27889  dmdbr  27894  cvmd  27931  cvexch  27969  sumdmdii  28010  mddmdin0i  28026  ofpreima2  28215  crefeq  28624  ldgenpisyslem1  28937  ldgenpisys  28940  inelsros  28952  diffiunisros  28953  elcarsg  29089  carsgclctunlem2  29103  carsgclctun  29105  ballotlemfval  29274  ballotlemgval  29308  ballotlemgvalOLD  29346  cvmscbv  29933  cvmsdisj  29945  cvmsss2  29949  nepss  30302  tailfb  30982  mblfinlem2  31885  lshpinN  32467  elrfi  35448  fipjust  36082  conrel1d  36168  csbresgVD  37208  disjf1  37361  fouriersw  37978  nnfoctbdjlem  38144  meadjun  38151  caragenel  38167