Theorem inteqd 4909

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

Syntax hints:   → wi 4   = wceq 1559  ∩ cint 4904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-ral 3076  df-rex 3086  df-int 4905

This theorem is referenced by:  elreldm  5909  ordintdif  6393  fniinfv  6941  onsucmin  7797  elxp5  7900  1stval2  7983  2ndval2  7984  naddcllem  8641  naddov2  8644  naddcom  8648  naddrid  8649  naddasslem1  8660  naddasslem2  8661  naddass  8662  naddsuc2  8667  fundmen  9008  xpsnen  9029  unblem2  9233  unblem3  9234  fiint  9267  elfi2  9357  fi0  9363  elfiun  9373  tcvalg  9688  tz9.12lem3  9744  rankvalb  9752  rankvalg  9772  ranksnb  9782  rankonidlem  9783  cardval3  9907  cardidm  9914  harsucnn  9953  cfval  10200  cflim3  10216  coftr  10227  isfin3ds  10283  fin23lem17  10292  fin23lem39  10304  isf33lem  10320  isf34lem5  10332  isf34lem6  10334  wuncval  10697  tskmval  10794  cleq1  14993  dfrtrcl2  15072  mrcfval  17623  mrcval  17625  cycsubg2  19234  efgval  19740  rgspnval  20641  lspfval  21020  lspval  21022  lsppropd  21065  aspval  21904  aspval2  21930  clsfval  23065  clsval  23077  clsval2  23090  hauscmplem  23446  cmpfi  23448  1stcfb  23485  fclscmp  24070  cutsval  27850  spanval  31482  chsupid  31561  intimafv  32863  fldgenval  33460  primefldgen1  33469  zarclsint  34130  zarcmplem  34139  sigagenval  34398  onvf1odlem3  35412  onvfowev  35423  kur14  35530  mclsval  35877  nmulprop  36504  nmulcom  36508  igenval  38524  pclfvalN  40477  pclvalN  40478  diaintclN  41646  docaffvalN  41709  docafvalN  41710  docavalN  41711  dibintclN  41755  dihglb2  41930  dihintcl  41932  mzpval  43277  dnnumch3lem  43587  aomclem8  43602  rp-intrabeq  43762  nadd1suc  43933  minregex2  44075  iotain  44957  salgenval  46859  mreclat  49582