Theorem ineq2i 3811

Description: Equality inference for intersection of two classes. (Contributed by NM, 26-Dec-1993.)

Hypothesis

Ref	Expression
ineq1i.1	|- A = B

Assertion

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

Proof of Theorem ineq2i

Step	Hyp	Ref	Expression
1		ineq1i.1	. 2 |- A = B
2		ineq2 3808	. 2 |- ( A = B -> ( C i^i A ) = ( C i^i B ) )
3	1, 2	ax-mp 5	1 |- ( C i^i A ) = ( C i^i B )

Syntax hints:   = 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:  in4  3829  inindir  3831  indif2  3870  difun1  3887  dfrab3ss  3905  undif1  4043  difdifdir  4056  dfif3  4100  dfif5  4102  disjpr2  4248  disjprsn  4250  disjtp2  4252  intunsn  4516  rint0  4517  riin0  4594  csbres  5399  res0  5400  resres  5409  resundi  5410  resindi  5412  inres  5414  resiun2  5418  resopab  5446  dffr3  5498  dfse2  5499  dminxp  5574  imainrect  5575  resdmres  5625  dfpred2  5689  predidm  5702  funimacnv  5970  fresaun  6075  fresaunres2  6076  wfrlem13  7427  tfrlem10  7483  sbthlem5  8074  infssuni  8257  dfsup2  8350  en3lplem2  8512  wemapwe  8594  epfrs  8607  r0weon  8835  infxpenlem  8836  kmlem11  8982  ackbij1lem1  9042  ackbij1lem2  9043  axdc3lem4  9275  canthwelem  9472  dmaddpi  9712  dmmulpi  9713  ssxr  10107  dmhashres  13129  fz1isolem  13245  f1oun2prg  13662  fsumiun  14553  sadeq  15194  bitsres  15195  smuval2  15204  smumul  15215  ressinbas  15936  lubdm  16979  glbdm  16992  sylow2a  18034  lsmmod2  18089  lsmdisj2r  18098  ablfac1eu  18472  ressmplbas2  19455  opsrtoslem1  19484  pjdm  20051  rintopn  20714  ordtrest2  21008  cmpsublem  21202  kgentopon  21341  hausdiag  21448  uzrest  21701  ufprim  21713  trust  22033  metnrmlem3  22664  clsocv  23049  ismbl  23294  unmbl  23305  volinun  23314  voliunlem1  23318  ovolioo  23336  itg2cnlem2  23529  ellimc2  23641  limcflf  23645  lhop1lem  23776  lgsquadlem3  25107  rplogsum  25216  umgrislfupgrlem  26017  spthispth  26622  0pth  26986  1pthdlem2  26996  frgrncvvdeqlem3  27165  ex-in  27282  chdmj3i  28342  chdmj4i  28343  chjassi  28345  pjoml2i  28444  pjoml3i  28445  cmcmlem  28450  cmcm2i  28452  cmbr3i  28459  fh3i  28482  fh4i  28483  osumcor2i  28503  mayetes3i  28588  mdslmd3i  29191  mdexchi  29194  atabsi  29260  dmdbr5ati  29281  inin  29352  uniin2  29368  ordtrest2NEW  29969  hasheuni  30147  carsgclctunlem1  30379  eulerpartgbij  30434  fiblem  30460  cvmscld  31255  msrid  31442  dfpo2  31645  elrn3  31652  noextend  31819  noextendseq  31820  madeval2  31936  bj-inrab3  32925  poimirlem15  33424  mblfinlem2  33447  ftc1anclem6  33490  pol0N  35195  mapfzcons2  37282  diophrw  37322  conrel2d  37956  iunrelexp0  37994  hashnzfz  38519  disjinfi  39380  fourierdlem80  40403  sge0resplit  40623  sge0split  40626  caragenuncllem  40726