Theorem inteqd 4911

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569  ∩ cint 4906

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-ral 3077  df-rex 3087  df-int 4907

This theorem is used by:  elreldm  5916  ordintdif  6414  fniinfv  6963  onsucmin  7832  elxp5  7935  1stval2  8018  2ndval2  8019  naddcllem  8688  naddov2  8691  naddcom  8695  naddrid  8696  naddasslem1  8707  naddasslem2  8708  naddass  8709  naddsuc2  8714  fundmen  9062  xpsnen  9083  unblem2  9288  unblem3  9289  fiint  9321  elfi2  9409  fi0  9415  elfiun  9425  tcvalg  9740  tz9.12lem3  9799  rankvalb  9808  rankvalg  9829  ranksnb  9840  rankonidlem  9841  cardval3  10036  cardidm  10043  harsucnn  10082  cfval  10327  cflim3  10343  coftr  10354  isfin3ds  10410  fin23lem17  10419  fin23lem39  10431  isf33lem  10447  isf34lem5  10459  isf34lem6  10461  wuncval  10830  tskmval  10927  cleq1  15141  dfrtrcl2  15220  mrcfval  17787  mrcval  17789  cycsubg2  19430  efgval  19936  rgspnval  20869  lspfval  21253  lspval  21255  lsppropd  21298  rspvalint  21528  aspval  22185  aspval2  22211  clsfval  23348  clsval  23360  clsval2  23373  hauscmplem  23729  cmpfi  23731  1stcfb  23768  fclscmp  24354  cutsval  28171  spanval  31940  chsupid  32019  intimafv  33351  fldgenval  33920  primefldgen1  33929  zarclsint  34550  zarcmplem  34559  sigagenval  34819  onvf1odlem3  35952  onprcf1acwevdlem2  35965  onvfowev  35969  onf1oracwevd  35971  kur14  36067  mclsval  36414  nmulprop  37031  nmulcom  37035  nmulrid  37038  igenval  39088  pclfvalN  41039  pclvalN  41040  diaintclN  42208  docaffvalN  42271  docafvalN  42272  docavalN  42273  dibintclN  42317  dihglb2  42492  dihintcl  42494  mzpval  43836  dnnumch3lem  44146  aomclem8  44156  rp-intrabeq  44316  nadd1suc  44487  minregex2  44629  iotain  45494  salgenval  47424  mreclat  50204