Theorem ineq2i 2214

Description: Equality inference for intersection of two classes.

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 2211	. 2 |- (A = B -> (C i^i A) = (C i^i B))
3	1, 2	ax-mp 7	1 |- (C i^i A) = (C i^i B)

Syntax hints:   = wceq 956   i^i cin 2046

This theorem is referenced by:  in23 2225  in4 2226  inindir 2228  difun1 2263  difab 2269  difin0 2338  undif1 2340  difdifdir 2346  intunsn 2565  dfepfr 2932  epfrc 2933  res0 3371  resres 3377  resundi 3378  resopab 3395  dffr3 3431  dminxp 3483  rescnvcnv 3493  resdmres 3497  funimacnv 3571  tfrlem10 3920  tz7.44-2 3929  tz7.44-3 3930  frfnom 3951  sbthlem5 4451  zfregs 4647  kmlem11 4775  dmaddpi 5018  dmmulpi 5019  renfdisj 5539  bastgt 7622  subtop 7646  cncfmet 7905  chdmj3 9406  chdmj4 9407  chjass 9409  pjoml2 9528  pjoml3 9529  cmcmlem 9534  cmcm2 9536  cmbr3 9543  fh3 9566  fh4 9567  osumcor2 9590  mdslmd3 10259  mdexch 10262  atabs 10328  dmdbr5at 10349

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812  df-in 2051

Copyright terms: Public domain