Theorem ineq2 3639

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

Syntax hints:   -> wi 4   = wceq 1454   i^i cin 3414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-v 3058  df-in 3422

This theorem is referenced by:  ineq12  3640  ineq2i  3642  ineq2d  3645  uneqin  3705  intprg  4282  wefrc  4846  onfr  5480  onnseq  7088  qsdisj  7465  disjenex  7755  fiint  7873  elfiun  7969  dffi3  7970  cplem2  8386  dfac5  8584  kmlem2  8606  kmlem13  8617  kmlem14  8618  ackbij1lem16  8690  fin23lem12  8786  fin23lem19  8791  fin23lem33  8800  uzin2  13455  pgpfac1lem3  17758  pgpfac1lem5  17760  pgpfac1  17761  inopn  19977  basis1  20013  basis2  20014  baspartn  20017  fctop  20067  cctop  20069  ordtbaslem  20252  hausnei2  20417  cnhaus  20418  nrmsep  20421  isnrm2  20422  dishaus  20446  ordthauslem  20447  dfcon2  20482  nconsubb  20486  finlocfin  20583  dissnlocfin  20592  locfindis  20593  kgeni  20600  pthaus  20701  txhaus  20710  xkohaus  20716  regr1lem  20802  fbasssin  20899  fbun  20903  fbunfip  20932  filcon  20946  isufil2  20971  ufileu  20982  filufint  20983  fmfnfmlem4  21020  fmfnfm  21021  fclsopni  21078  fclsbas  21084  fclsrest  21087  isfcf  21097  tsmsfbas  21190  ustincl  21270  ust0  21282  metreslem  21425  methaus  21583  qtopbaslem  21827  metnrmlem3  21926  metnrmlem3OLD  21941  ismbl  22528  shincl  27082  chincl  27200  chdmm1  27226  ledi  27241  cmbr  27285  cmbr3i  27301  cmbr3  27309  pjoml2  27312  stcltrlem1  27977  mdbr  27995  dmdbr  28000  cvmd  28037  cvexch  28075  sumdmdii  28116  mddmdin0i  28132  ofpreima2  28317  crefeq  28720  ldgenpisyslem1  29033  ldgenpisys  29036  inelsros  29048  diffiunisros  29049  elcarsg  29185  carsgclctunlem2  29199  carsgclctun  29201  ballotlemfval  29370  ballotlemgval  29404  ballotlemgvalOLD  29442  cvmscbv  30029  cvmsdisj  30041  cvmsss2  30045  nepss  30398  tailfb  31081  mblfinlem2  32022  lshpinN  32599  elrfi  35580  fipjust  36213  conrel1d  36299  csbresgVD  37331  disjf1  37494  qinioo  37674  fouriersw  38132  nnfoctbdjlem  38330  meadjun  38337  caragenel  38353