Theorem ineq2i 3599

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 3596	. 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 1448   i^i cin 3371

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-clab 2439  df-cleq 2445  df-clel 2448  df-nfc 2582  df-v 3015  df-in 3379

This theorem is referenced by:  in4  3616  inindir  3618  indif2  3654  difun1  3671  dfrab3ss  3689  undif1  3810  difdifdir  3823  dfif3  3863  dfif5  3865  disjprsn  4003  intunsn  4244  rint0  4245  riin0  4322  csbres  5086  res0  5087  resres  5095  resundi  5096  resindi  5098  inres  5100  resiun2  5102  resopab  5129  dffr3  5179  dfse2  5180  dminxp  5255  imainrect  5256  resdmres  5305  dfpred2  5368  predidm  5381  funimacnv  5637  fresaun  5737  fresaunres2  5738  wfrlem13  7035  tfrlem10  7092  sbthlem5  7673  infssuni  7852  dfsup2  7945  en3lplem2  8107  wemapwe  8189  epfrs  8202  r0weon  8430  infxpenlem  8431  kmlem11  8577  ackbij1lem1  8637  ackbij1lem2  8638  axdc3lem4  8870  canthwelem  9062  dmaddpi  9302  dmmulpi  9303  ssxr  9690  dmhashres  12518  fz1isolem  12619  f1oun2prg  13010  fsumiun  13892  sadeq  14457  bitsres  14458  smuval2  14467  smumul  14478  ressinbas  15196  lubdm  16236  glbdm  16249  sylow2a  17282  lsmmod2  17337  lsmdisj2r  17346  ablfac1eu  17717  ressmplbas2  18690  opsrtoslem1  18718  pjdm  19281  rintopn  19950  ordtrest2  20231  cmpsublem  20425  kgentopon  20564  hausdiag  20671  uzrest  20923  ufprim  20935  trust  21255  metnrmlem3  21889  metnrmlem3OLD  21904  clsocv  22232  ismbl  22491  unmbl  22502  volinun  22511  voliunlem1  22515  ovolioo  22533  itg2cnlem2  22732  ellimc2  22844  limcflf  22848  lhop1lem  22977  lgsquadlem3  24296  rplogsum  24377  0pth  25312  1pthonlem2  25332  frgrancvvdeqlem4  25773  ex-in  25887  chdmj3i  27148  chdmj4i  27149  chjassi  27151  pjoml2i  27250  pjoml3i  27251  cmcmlem  27256  cmcm2i  27258  cmbr3i  27265  fh3i  27288  fh4i  27289  osumcor2i  27309  mayetes3i  27394  mdslmd3i  27997  mdexchi  28000  atabsi  28066  dmdbr5ati  28087  inin  28161  uniin2  28176  ordtrest2NEW  28736  hasheuni  28913  carsgclctunlem1  29155  eulerpartgbij  29211  fiblem  29237  cvmscld  30002  msrid  30189  dfpo2  30401  elrn3  30409  bj-inrab3  31534  poimirlem15  31957  mblfinlem2  31980  ftc1anclem6  32024  pol0N  33476  mapfzcons2  35563  diophrw  35603  conrel2d  36258  iunrelexp0  36296  hashnzfz  36670  disjinfi  37478  fourierdlem80  38107  sge0resplit  38307  sge0split  38310  caragenuncllem  38397  umgrislfupgrlem  39770  sPthisPth  39812  0pth-av  39893  1pthdlem2  39903