Theorem ineq2 3534

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

Syntax hints:   -> wi 4   = wceq 1362   i^i cin 3315

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-in 3323

This theorem is referenced by:  ineq12  3535  ineq2i  3537  ineq2d  3540  uneqin  3589  intprg  4150  wefrc  4701  onfr  4745  onnseq  6791  qsdisj  7165  disjenex  7457  fiint  7576  elfiun  7668  dffi3  7669  cplem2  8085  dfac5  8286  kmlem2  8308  kmlem13  8319  kmlem14  8320  ackbij1lem16  8392  fin23lem12  8488  fin23lem19  8493  fin23lem33  8502  uzin2  12816  pgpfac1lem3  16552  pgpfac1lem5  16554  pgpfac1  16555  inopn  18354  basis1  18397  basis2  18398  baspartn  18401  fctop  18450  cctop  18452  ordtbaslem  18634  hausnei2  18799  cnhaus  18800  nrmsep  18803  isnrm2  18804  dishaus  18828  ordthauslem  18829  bwthOLD  18856  dfcon2  18865  nconsubb  18869  kgeni  18952  pthaus  19053  txhaus  19062  xkohaus  19068  regr1lem  19154  fbasssin  19251  fbun  19255  fbunfip  19284  filcon  19298  isufil2  19323  ufileu  19334  filufint  19335  fmfnfmlem4  19372  fmfnfm  19373  fclsopni  19430  fclsbas  19436  fclsrest  19439  isfcf  19449  tsmsfbas  19540  ustincl  19624  ust0  19636  metreslem  19779  methaus  19937  qtopbaslem  20179  metnrmlem3  20279  ismbl  20851  shincl  24607  chincl  24725  chdmm1  24751  ledi  24766  cmbr  24810  cmbr3i  24826  cmbr3  24834  pjoml2  24837  stcltrlem1  25503  mdbr  25521  dmdbr  25526  cvmd  25563  cvexch  25601  sumdmdii  25642  mddmdin0i  25658  ofpreima2  25809  ballotlemfval  26720  ballotlemgval  26754  cvmscbv  26995  cvmsdisj  27007  cvmsss2  27011  nepss  27221  mblfinlem2  28273  finlocfin  28415  locfindis  28421  tailfb  28442  elrfi  28875  csbresgVD  31333  lshpinN  32207