Theorem inteqd 4954

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 4952	. 2 ⊢ (𝐴 = 𝐵 → ∩ 𝐴 = ∩ 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → ∩ 𝐴 = ∩ 𝐵)

Syntax hints:   → wi 4   = wceq 1534  ∩ cint 4949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-ral 3059  df-rex 3068  df-int 4950

This theorem is referenced by:  intprgOLD  4987  elreldm  5937  ordintdif  6419  fniinfv  6976  onsucmin  7824  elxp5  7931  1stval2  8010  2ndval2  8011  naddcllem  8696  naddov2  8699  naddcom  8702  naddrid  8703  naddasslem1  8714  naddasslem2  8715  naddass  8716  fundmen  9055  xpsnen  9079  unblem2  9320  unblem3  9321  fiint  9348  elfi2  9437  fi0  9443  elfiun  9453  tcvalg  9761  tz9.12lem3  9812  rankvalb  9820  rankvalg  9840  ranksnb  9850  rankonidlem  9851  cardval3  9975  cardidm  9982  harsucnn  10021  cfval  10270  cflim3  10285  coftr  10296  isfin3ds  10352  fin23lem17  10361  fin23lem39  10373  isf33lem  10389  isf34lem5  10401  isf34lem6  10403  wuncval  10765  tskmval  10862  cleq1  14962  dfrtrcl2  15041  mrcfval  17587  mrcval  17589  cycsubg2  19164  efgval  19671  lspfval  20856  lspval  20858  lsppropd  20902  aspval  21805  aspval2  21830  clsfval  22928  clsval  22940  clsval2  22953  hauscmplem  23309  cmpfi  23311  1stcfb  23348  fclscmp  23933  scutval  27732  spanval  31142  chsupid  31221  intimafv  32490  fldgenval  32999  primefldgen1  33008  zarclsint  33473  zarcmplem  33482  sigagenval  33759  kur14  34826  mclsval  35173  igenval  37534  pclfvalN  39362  pclvalN  39363  diaintclN  40531  docaffvalN  40594  docafvalN  40595  docavalN  40596  dibintclN  40640  dihglb2  40815  dihintcl  40817  mzpval  42152  dnnumch3lem  42470  aomclem8  42485  rgspnval  42592  rp-intrabeq  42649  nadd1suc  42821  naddsuc2  42822  minregex2  42965  iotain  43854  salgenval  45709  mreclat  48008