Theorem ineq2 2207

Description: Equality theorem for intersection of two classes.

Assertion

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

Proof of Theorem ineq2

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

Syntax hints:   -> wi 3   = wceq 954   i^i cin 2042

This theorem is referenced by:  ineq12 2208  ineq2i 2210  ineq2d 2213  uneqin 2252  wefrc 2938  onfr 2981  fiint 4540  cplem2 4701  aceq5 4720  kmlem2 4746  kmlem13 4757  kmlem14 4758  inopnt 7550  basis1t 7564  basis2t 7565  sn0top 7597  fctop 7600  cctop 7602  metres 7775  methausi 7833  shinclt 9289  chinclt 9360  chdmm1t 9386  ledit 9401  cmbrt 9467  cmbr3 9483  cmbr3t 9491  pjoml2t 9494  stcltrlem1 10141  mdbrt 10159  dmdbrt 10164  cvmdt 10200  cvexcht 10238  sumdmdi 10278  mddmdin0 10292  infi1 10383  intprd 10403  neiopne 10405  subsp 10465  filint 10473  filintf 10479  cnfilca 10487  dtt2 10498  ishgrag 10641  hgralem 10642  ispgrag 10651

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-v 1808  df-in 2047

Copyright terms: Public domain