Theorem ineq2 3687

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

Syntax hints:   -> wi 4   = wceq 1374   i^i cin 3468

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-v 3108  df-in 3476

This theorem is referenced by:  ineq12  3688  ineq2i  3690  ineq2d  3693  uneqin  3742  intprg  4309  wefrc  4866  onfr  4910  onnseq  7005  qsdisj  7378  disjenex  7665  fiint  7786  elfiun  7879  dffi3  7880  cplem2  8297  dfac5  8498  kmlem2  8520  kmlem13  8531  kmlem14  8532  ackbij1lem16  8604  fin23lem12  8700  fin23lem19  8705  fin23lem33  8714  uzin2  13126  pgpfac1lem3  16911  pgpfac1lem5  16913  pgpfac1  16914  inopn  19168  basis1  19211  basis2  19212  baspartn  19215  fctop  19264  cctop  19266  ordtbaslem  19448  hausnei2  19613  cnhaus  19614  nrmsep  19617  isnrm2  19618  dishaus  19642  ordthauslem  19643  bwthOLD  19670  dfcon2  19679  nconsubb  19683  kgeni  19766  pthaus  19867  txhaus  19876  xkohaus  19882  regr1lem  19968  fbasssin  20065  fbun  20069  fbunfip  20098  filcon  20112  isufil2  20137  ufileu  20148  filufint  20149  fmfnfmlem4  20186  fmfnfm  20187  fclsopni  20244  fclsbas  20250  fclsrest  20253  isfcf  20263  tsmsfbas  20354  ustincl  20438  ust0  20450  metreslem  20593  methaus  20751  qtopbaslem  20993  metnrmlem3  21093  ismbl  21665  shincl  25961  chincl  26079  chdmm1  26105  ledi  26120  cmbr  26164  cmbr3i  26180  cmbr3  26188  pjoml2  26191  stcltrlem1  26857  mdbr  26875  dmdbr  26880  cvmd  26917  cvexch  26955  sumdmdii  26996  mddmdin0i  27012  ofpreima2  27166  ballotlemfval  28054  ballotlemgval  28088  cvmscbv  28329  cvmsdisj  28341  cvmsss2  28345  nepss  28556  mblfinlem2  29616  finlocfin  29758  locfindis  29764  tailfb  29785  elrfi  30217  fouriersw  31487  csbresgVD  32650  lshpinN  33661  fipjust  36645  conrel1d  36656