Theorem ineq2 3608

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

Syntax hints:   -> wi 4   = wceq 1399   i^i cin 3388

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-v 3036  df-in 3396

This theorem is referenced by:  ineq12  3609  ineq2i  3611  ineq2d  3614  uneqin  3674  intprg  4234  wefrc  4787  onfr  4831  onnseq  6933  qsdisj  7306  disjenex  7594  fiint  7712  elfiun  7805  dffi3  7806  cplem2  8221  dfac5  8422  kmlem2  8444  kmlem13  8455  kmlem14  8456  ackbij1lem16  8528  fin23lem12  8624  fin23lem19  8629  fin23lem33  8638  uzin2  13179  pgpfac1lem3  17241  pgpfac1lem5  17243  pgpfac1  17244  inopn  19493  basis1  19536  basis2  19537  baspartn  19540  fctop  19590  cctop  19592  ordtbaslem  19775  hausnei2  19940  cnhaus  19941  nrmsep  19944  isnrm2  19945  dishaus  19969  ordthauslem  19970  dfcon2  20005  nconsubb  20009  finlocfin  20106  dissnlocfin  20115  locfindis  20116  kgeni  20123  pthaus  20224  txhaus  20233  xkohaus  20239  regr1lem  20325  fbasssin  20422  fbun  20426  fbunfip  20455  filcon  20469  isufil2  20494  ufileu  20505  filufint  20506  fmfnfmlem4  20543  fmfnfm  20544  fclsopni  20601  fclsbas  20607  fclsrest  20610  isfcf  20620  tsmsfbas  20711  ustincl  20795  ust0  20807  metreslem  20950  methaus  21108  qtopbaslem  21350  metnrmlem3  21450  ismbl  22022  shincl  26416  chincl  26534  chdmm1  26560  ledi  26575  cmbr  26619  cmbr3i  26635  cmbr3  26643  pjoml2  26646  stcltrlem1  27311  mdbr  27329  dmdbr  27334  cvmd  27371  cvexch  27409  sumdmdii  27450  mddmdin0i  27466  ofpreima2  27654  crefeq  28002  elcarsg  28432  carsgclctunlem2  28446  carsgclctun  28448  ballotlemfval  28611  ballotlemgval  28645  cvmscbv  28892  cvmsdisj  28904  cvmsss2  28908  nepss  29261  mblfinlem2  30217  tailfb  30361  elrfi  30792  fouriersw  32180  csbresgVD  34042  lshpinN  35127  fipjust  38179  conrel1d  38192