Theorem inteqd 4889

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

Syntax hints:   → wi 4   = wceq 1547  ∩ cint 4884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-ral 3055  df-rex 3065  df-int 4885

This theorem is referenced by:  elreldm  5884  ordintdif  6368  fniinfv  6912  onsucmin  7768  elxp5  7870  1stval2  7955  2ndval2  7956  naddcllem  8609  naddov2  8612  naddcom  8615  naddrid  8616  naddasslem1  8627  naddasslem2  8628  naddass  8629  naddsuc2  8634  fundmen  8975  xpsnen  8996  unblem2  9200  unblem3  9201  fiint  9234  elfi2  9324  fi0  9330  elfiun  9340  tcvalg  9655  tz9.12lem3  9711  rankvalb  9719  rankvalg  9739  ranksnb  9749  rankonidlem  9750  cardval3  9874  cardidm  9881  harsucnn  9920  cfval  10167  cflim3  10182  coftr  10193  isfin3ds  10249  fin23lem17  10258  fin23lem39  10270  isf33lem  10286  isf34lem5  10298  isf34lem6  10300  wuncval  10663  tskmval  10760  cleq1  14943  dfrtrcl2  15022  mrcfval  17572  mrcval  17574  cycsubg2  19183  efgval  19690  rgspnval  20591  lspfval  20970  lspval  20972  lsppropd  21015  aspval  21854  aspval2  21880  clsfval  23015  clsval  23027  clsval2  23040  hauscmplem  23396  cmpfi  23398  1stcfb  23435  fclscmp  24020  cutsval  27797  spanval  31429  chsupid  31508  intimafv  32810  fldgenval  33403  primefldgen1  33412  zarclsint  34063  zarcmplem  34072  sigagenval  34331  onvf1odlem3  35340  kur14  35451  mclsval  35798  igenval  38435  pclfvalN  40388  pclvalN  40389  diaintclN  41557  docaffvalN  41620  docafvalN  41621  docavalN  41622  dibintclN  41666  dihglb2  41841  dihintcl  41843  mzpval  43188  dnnumch3lem  43498  aomclem8  43513  rp-intrabeq  43673  nadd1suc  43844  minregex2  43986  iotain  44868  salgenval  46771  mreclat  49494