Theorem ineq2i 3006

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 3003	. 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 1586   i^i cin 2826

This theorem is referenced by:  in4 3022  inindir 3024  indif2 3047  difun1 3062  undif1 3149  difdifdir 3156  intunsn 3435  dfepfr 3796  epfrc 3797  res0 4344  resres 4350  resundi 4351  resindi 4353  inres 4355  resopab 4373  dffr3 4415  dminxp 4462  resdmres 4492  funimacnv 4590  tfrlem10 5292  tz7.44-2 5301  tz7.44-3 5302  frfnom 5323  sbthlem5 5680  dfsup2 5889  dfsup2OLD 5890  dfsup3OLD 5891  zfregs 5990  infxpenlem 6147  cdainf 6258  axdc3lem4 6308  kmlem11 6347  dmaddpi 6536  dmmulpi 6537  ssxr 6899  bastg 9743  subtop 9767  cncfmet 10049  tx1cn 11058  tx2cn 11059  fbssint 11117  chdmj3i 11873  chdmj4i 11874  chjassi 11876  pjoml2i 11993  pjoml3i 11994  cmcmlem 11999  cmcm2i 12001  cmbr3i 12008  fh3i 12031  fh4i 12032  osumcor2i 12057  mayetes3i 12142  mdslmd3i 12735  mdexchi 12738  atabsi 12804  dmdbr5ati 12825  dfpo2 14465  dfpred2 14528  predidm 14542  wfrlem13 14622  isunscov 15096  empos 15322  inposet 15359  dispos 15371  bwt2 15738  intopcon 15742  singempcon 15743  compsublem 16254  iccbnd 16850  pol0 18326

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-ex 1616  df-sb 1816  df-clab 2129  df-cleq 2134  df-clel 2137  df-v 2540  df-in 2834

Copyright terms: Public domain