Theorem ineq2i 3693

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 3690	. 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 1395   i^i cin 3470

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-in 3478

This theorem is referenced by:  in4  3710  inindir  3712  indif2  3748  difun1  3765  dfrab3ss  3783  undif1  3906  difdifdir  3918  dfif3  3958  dfif5  3960  intunsn  4328  rint0  4329  riin0  4406  csbres  5286  res0  5288  resres  5296  resundi  5297  resindi  5299  inres  5301  resiun2  5303  resopab  5330  dffr3  5379  dfse2  5380  dminxp  5454  imainrect  5455  resdmres  5504  funimacnv  5666  fresaun  5762  fresaunres2  5763  tfrlem10  7074  sbthlem5  7650  infssuni  7829  dfsup2  7920  dfsup2OLD  7921  en3lplem2  8049  wemapwe  8156  wemapweOLD  8157  epfrs  8179  r0weon  8407  infxpenlem  8408  kmlem11  8557  ackbij1lem1  8617  ackbij1lem2  8618  axdc3lem4  8850  canthwelem  9045  dmaddpi  9285  dmmulpi  9286  ssxr  9671  dmhashres  12417  fz1isolem  12514  f1oun2prg  12877  fsumiun  13647  sadeq  14134  bitsres  14135  smuval2  14144  smumul  14155  ressinbas  14707  lubdm  15736  glbdm  15749  sylow2a  16766  lsmmod2  16821  lsmdisj2r  16830  ablfac1eu  17251  ressmplbas2  18244  opsrtoslem1  18275  pjdm  18865  rintopn  19545  ordtrest2  19832  cmpsublem  20026  kgentopon  20165  hausdiag  20272  uzrest  20524  ufprim  20536  trust  20858  metnrmlem3  21491  clsocv  21816  ismbl  22063  unmbl  22074  volinun  22082  voliunlem1  22086  ovolioo  22104  itg2cnlem2  22295  ellimc2  22407  limcflf  22411  lhop1lem  22540  lgsquadlem3  23757  rplogsum  23838  0pth  24699  1pthonlem2  24719  frgrancvvdeqlem4  25160  ex-in  25273  chdmj3i  26528  chdmj4i  26529  chjassi  26531  pjoml2i  26630  pjoml3i  26631  cmcmlem  26636  cmcm2i  26638  cmbr3i  26645  fh3i  26668  fh4i  26669  osumcor2i  26689  mayetes3i  26775  mdslmd3i  27378  mdexchi  27381  atabsi  27447  dmdbr5ati  27468  inin  27541  ordtrest2NEW  28066  hasheuni  28257  carsgclctunlem1  28460  eulerpartgbij  28508  fiblem  28534  cvmscld  28915  msrid  29102  dfpo2  29402  elrn3  29410  dfpred2  29470  predidm  29485  wfrlem13  29572  mblfinlem2  30257  ftc1anclem6  30300  mapfzcons2  30856  diophrw  30897  hashnzfz  31429  fourierdlem80  32172  pol0N  35776  conrel2d  37922