Theorem inteqd 4951

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

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

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 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-ral 3062  df-rex 3071  df-int 4947

This theorem is referenced by:  elreldm  5946  ordintdif  6434  fniinfv  6987  onsucmin  7841  elxp5  7945  1stval2  8031  2ndval2  8032  naddcllem  8714  naddov2  8717  naddcom  8720  naddrid  8721  naddasslem1  8732  naddasslem2  8733  naddass  8734  naddsuc2  8739  fundmen  9071  xpsnen  9095  unblem2  9329  unblem3  9330  fiint  9366  fiintOLD  9367  elfi2  9454  fi0  9460  elfiun  9470  tcvalg  9778  tz9.12lem3  9829  rankvalb  9837  rankvalg  9857  ranksnb  9867  rankonidlem  9868  cardval3  9992  cardidm  9999  harsucnn  10038  cfval  10287  cflim3  10302  coftr  10313  isfin3ds  10369  fin23lem17  10378  fin23lem39  10390  isf33lem  10406  isf34lem5  10418  isf34lem6  10420  wuncval  10782  tskmval  10879  cleq1  15022  dfrtrcl2  15101  mrcfval  17651  mrcval  17653  cycsubg2  19228  efgval  19735  rgspnval  20612  lspfval  20971  lspval  20973  lsppropd  21017  aspval  21893  aspval2  21918  clsfval  23033  clsval  23045  clsval2  23058  hauscmplem  23414  cmpfi  23416  1stcfb  23453  fclscmp  24038  scutval  27845  spanval  31352  chsupid  31431  intimafv  32720  fldgenval  33314  primefldgen1  33323  zarclsint  33871  zarcmplem  33880  sigagenval  34141  kur14  35221  mclsval  35568  igenval  38068  pclfvalN  39891  pclvalN  39892  diaintclN  41060  docaffvalN  41123  docafvalN  41124  docavalN  41125  dibintclN  41169  dihglb2  41344  dihintcl  41346  mzpval  42743  dnnumch3lem  43058  aomclem8  43073  rp-intrabeq  43233  nadd1suc  43405  minregex2  43548  iotain  44436  salgenval  46336  mreclat  48886