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 1542  ∩ cint 4904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-ral 3053  df-rex 3063  df-int 4905

This theorem is referenced by:  elreldm  5892  ordintdif  6376  fniinfv  6920  onsucmin  7773  elxp5  7875  1stval2  7960  2ndval2  7961  naddcllem  8614  naddov2  8617  naddcom  8620  naddrid  8621  naddasslem1  8632  naddasslem2  8633  naddass  8634  naddsuc2  8639  fundmen  8980  xpsnen  9001  unblem2  9205  unblem3  9206  fiint  9239  elfi2  9329  fi0  9335  elfiun  9345  tcvalg  9657  tz9.12lem3  9713  rankvalb  9721  rankvalg  9741  ranksnb  9751  rankonidlem  9752  cardval3  9876  cardidm  9883  harsucnn  9922  cfval  10169  cflim3  10184  coftr  10195  isfin3ds  10251  fin23lem17  10260  fin23lem39  10272  isf33lem  10288  isf34lem5  10300  isf34lem6  10302  wuncval  10665  tskmval  10762  cleq1  14918  dfrtrcl2  14997  mrcfval  17543  mrcval  17545  cycsubg2  19151  efgval  19658  rgspnval  20557  lspfval  20936  lspval  20938  lsppropd  20982  aspval  21840  aspval2  21866  clsfval  22981  clsval  22993  clsval2  23006  hauscmplem  23362  cmpfi  23364  1stcfb  23401  fclscmp  23986  cutsval  27788  spanval  31420  chsupid  31499  intimafv  32800  fldgenval  33405  primefldgen1  33414  zarclsint  34049  zarcmplem  34058  sigagenval  34317  onvf1odlem3  35318  kur14  35429  mclsval  35776  igenval  38306  pclfvalN  40259  pclvalN  40260  diaintclN  41428  docaffvalN  41491  docafvalN  41492  docavalN  41493  dibintclN  41537  dihglb2  41712  dihintcl  41714  mzpval  43083  dnnumch3lem  43397  aomclem8  43412  rp-intrabeq  43572  nadd1suc  43743  minregex2  43885  iotain  44767  salgenval  46673  mreclat  49350