Theorem ineq2 3808

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

Syntax hints:   -> wi 4   = wceq 1483   i^i cin 3573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581

This theorem is referenced by:  ineq12  3809  ineq2i  3811  ineq2d  3814  uneqin  3878  intprg  4511  wefrc  5108  onfr  5763  onnseq  7441  qsdisj  7824  disjenex  8118  fiint  8237  elfiun  8336  dffi3  8337  cplem2  8753  dfac5  8951  kmlem2  8973  kmlem13  8984  kmlem14  8985  ackbij1lem16  9057  fin23lem12  9153  fin23lem19  9158  fin23lem33  9167  uzin2  14084  pgpfac1lem3  18476  pgpfac1lem5  18478  pgpfac1  18479  inopn  20704  basis1  20754  basis2  20755  baspartn  20758  fctop  20808  cctop  20810  ordtbaslem  20992  hausnei2  21157  cnhaus  21158  nrmsep  21161  isnrm2  21162  dishaus  21186  ordthauslem  21187  dfconn2  21222  nconnsubb  21226  finlocfin  21323  dissnlocfin  21332  locfindis  21333  kgeni  21340  pthaus  21441  txhaus  21450  xkohaus  21456  regr1lem  21542  fbasssin  21640  fbun  21644  fbunfip  21673  filconn  21687  isufil2  21712  ufileu  21723  filufint  21724  fmfnfmlem4  21761  fmfnfm  21762  fclsopni  21819  fclsbas  21825  fclsrest  21828  isfcf  21838  tsmsfbas  21931  ustincl  22011  ust0  22023  metreslem  22167  methaus  22325  qtopbaslem  22562  metnrmlem3  22664  ismbl  23294  shincl  28240  chincl  28358  chdmm1  28384  ledi  28399  cmbr  28443  cmbr3i  28459  cmbr3  28467  pjoml2  28470  stcltrlem1  29135  mdbr  29153  dmdbr  29158  cvmd  29195  cvexch  29233  sumdmdii  29274  mddmdin0i  29290  ofpreima2  29466  crefeq  29912  ldgenpisyslem1  30226  ldgenpisys  30229  inelsros  30241  diffiunisros  30242  elcarsg  30367  carsgclctunlem2  30381  carsgclctun  30383  ballotlemfval  30551  ballotlemgval  30585  cvmscbv  31240  cvmsdisj  31252  cvmsss2  31256  nepss  31599  tailfb  32372  bj-0int  33055  mblfinlem2  33447  lshpinN  34276  elrfi  37257  fipjust  37870  conrel1d  37955  ntrk0kbimka  38337  clsk3nimkb  38338  isotone2  38347  ntrclskb  38367  ntrclsk3  38368  ntrclsk13  38369  csbresgVD  39131  disjf1  39369  qinioo  39762  fouriersw  40448  nnfoctbdjlem  40672  meadjun  40679  caragenel  40709