Theorem inteqd 4415

Description: Equality deduction for class intersection. (Contributed by NM, 2-Sep-2003.)

Hypothesis

Ref	Expression
inteqd.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
inteqd	⊢ (𝜑 → ∩ 𝐴 = ∩ 𝐵)

Proof of Theorem inteqd

Step	Hyp	Ref	Expression
1		inteqd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		inteq 4413	. 2 ⊢ (𝐴 = 𝐵 → ∩ 𝐴 = ∩ 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → ∩ 𝐴 = ∩ 𝐵)

Syntax hints:   → wi 4   = wceq 1475  ∩ cint 4410

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-int 4411

This theorem is referenced by:  intprg  4446  elreldm  5271  ordintdif  5691  fniinfv  6167  onsucmin  6913  elxp5  7004  1stval2  7076  2ndval2  7077  fundmen  7916  xpsnen  7929  unblem2  8098  unblem3  8099  fiint  8122  elfi2  8203  fi0  8209  elfiun  8219  tcvalg  8497  tz9.12lem3  8535  rankvalb  8543  rankvalg  8563  ranksnb  8573  rankonidlem  8574  cardval3  8661  cardidm  8668  cfval  8952  cflim3  8967  coftr  8978  isfin3ds  9034  fin23lem17  9043  fin23lem39  9055  isf33lem  9071  isf34lem5  9083  isf34lem6  9085  wuncval  9443  tskmval  9540  cleq1  13570  dfrtrcl2  13650  mrcfval  16091  mrcval  16093  cycsubg2  17454  efgval  17953  lspfval  18794  lspval  18796  lsppropd  18839  aspval  19149  aspval2  19168  clsfval  20639  clsval  20651  clsval2  20664  hauscmplem  21019  cmpfi  21021  1stcfb  21058  fclscmp  21644  spanval  27576  chsupid  27655  sigagenval  29530  kur14  30452  mclsval  30714  igenval  33030  pclfvalN  34193  pclvalN  34194  diaintclN  35365  docaffvalN  35428  docafvalN  35429  docavalN  35430  dibintclN  35474  dihglb2  35649  dihintcl  35651  mzpval  36313  dnnumch3lem  36634  aomclem8  36649  rgspnval  36757  iotain  37640  salgenval  39217