Theorem inteqd 4904

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

Syntax hints:   → wi 4   = wceq 1540  ∩ cint 4899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-ral 3045  df-rex 3054  df-int 4900

This theorem is referenced by:  elreldm  5881  ordintdif  6362  fniinfv  6905  onsucmin  7760  elxp5  7863  1stval2  7948  2ndval2  7949  naddcllem  8601  naddov2  8604  naddcom  8607  naddrid  8608  naddasslem1  8619  naddasslem2  8620  naddass  8621  naddsuc2  8626  fundmen  8963  xpsnen  8985  unblem2  9198  unblem3  9199  fiint  9235  fiintOLD  9236  elfi2  9323  fi0  9329  elfiun  9339  tcvalg  9653  tz9.12lem3  9704  rankvalb  9712  rankvalg  9732  ranksnb  9742  rankonidlem  9743  cardval3  9867  cardidm  9874  harsucnn  9913  cfval  10160  cflim3  10175  coftr  10186  isfin3ds  10242  fin23lem17  10251  fin23lem39  10263  isf33lem  10279  isf34lem5  10291  isf34lem6  10293  wuncval  10655  tskmval  10752  cleq1  14908  dfrtrcl2  14987  mrcfval  17532  mrcval  17534  cycsubg2  19107  efgval  19614  rgspnval  20515  lspfval  20894  lspval  20896  lsppropd  20940  aspval  21798  aspval2  21823  clsfval  22928  clsval  22940  clsval2  22953  hauscmplem  23309  cmpfi  23311  1stcfb  23348  fclscmp  23933  scutval  27729  spanval  31295  chsupid  31374  intimafv  32667  fldgenval  33261  primefldgen1  33270  zarclsint  33838  zarcmplem  33847  sigagenval  34106  onvf1odlem3  35077  kur14  35188  mclsval  35535  igenval  38040  pclfvalN  39868  pclvalN  39869  diaintclN  41037  docaffvalN  41100  docafvalN  41101  docavalN  41102  dibintclN  41146  dihglb2  41321  dihintcl  41323  mzpval  42705  dnnumch3lem  43019  aomclem8  43034  rp-intrabeq  43194  nadd1suc  43365  minregex2  43508  iotain  44390  salgenval  46303  mreclat  48982