Theorem inteqd 4913

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

Syntax hints:   → wi 4   = wceq 1563  ∩ cint 4908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-ral 3080  df-rex 3090  df-int 4909

This theorem is referenced by:  elreldm  5916  ordintdif  6401  fniinfv  6949  onsucmin  7805  elxp5  7908  1stval2  7991  2ndval2  7992  naddcllem  8650  naddov2  8653  naddcom  8657  naddrid  8658  naddasslem1  8669  naddasslem2  8670  naddass  8671  naddsuc2  8676  fundmen  9016  xpsnen  9037  unblem2  9241  unblem3  9242  fiint  9274  elfi2  9362  fi0  9368  elfiun  9378  tcvalg  9693  tz9.12lem3  9749  rankvalb  9757  rankvalg  9777  ranksnb  9787  rankonidlem  9788  cardval3  9926  cardidm  9933  harsucnn  9972  cfval  10218  cflim3  10234  coftr  10245  isfin3ds  10301  fin23lem17  10310  fin23lem39  10322  isf33lem  10338  isf34lem5  10350  isf34lem6  10352  wuncval  10715  tskmval  10812  cleq1  15010  dfrtrcl2  15089  mrcfval  17654  mrcval  17656  cycsubg2  19272  efgval  19778  rgspnval  20688  lspfval  21063  lspval  21065  lsppropd  21108  aspval  21982  aspval2  22008  clsfval  23143  clsval  23155  clsval2  23168  hauscmplem  23524  cmpfi  23526  1stcfb  23563  fclscmp  24148  cutsval  27931  spanval  31594  chsupid  31673  intimafv  32968  fldgenval  33548  primefldgen1  33557  zarclsint  34179  zarcmplem  34188  sigagenval  34447  onvf1odlem3  35460  onvfowev  35471  kur14  35579  mclsval  35926  nmulprop  36553  nmulcom  36557  igenval  38572  pclfvalN  40525  pclvalN  40526  diaintclN  41694  docaffvalN  41757  docafvalN  41758  docavalN  41759  dibintclN  41803  dihglb2  41978  dihintcl  41980  mzpval  43325  dnnumch3lem  43635  aomclem8  43650  rp-intrabeq  43810  nadd1suc  43981  minregex2  44123  iotain  44991  salgenval  46893  mreclat  49626