Theorem inteqd 4915

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ∩ cint 4910

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-ral 3081  df-rex 3091  df-int 4911

This theorem is used by:  elreldm  5924  ordintdif  6432  iotain  6531  fniinfv  6986  onsucmin  7856  elxp5  7959  1stval2  8042  2ndval2  8043  naddcllem  8713  naddov2  8716  naddcom  8720  naddrid  8721  naddasslem1  8732  naddasslem2  8733  naddass  8734  naddsuc2  8739  fundmen  9087  xpsnen  9108  unblem2  9313  unblem3  9314  fiint  9346  elfi2  9433  fi0  9439  elfiun  9449  tcvalg  9764  tz9.12lem3  9823  rankvalb  9832  rankvalg  9853  ranksnb  9864  rankonidlem  9865  cardval3  10060  cardidm  10067  harsucnn  10106  cfval  10351  cflim3  10367  coftr  10378  isfin3ds  10434  fin23lem17  10443  fin23lem39  10455  isf33lem  10471  isf34lem5  10483  isf34lem6  10485  wuncval  10854  tskmval  10951  cleq1  15165  dfrtrcl2  15244  mrcfval  17811  mrcval  17813  cycsubg2  19454  efgval  19961  rgspnval  20894  lspfval  21278  lspval  21280  lsppropd  21323  rspvalint  21553  aspval  22210  aspval2  22236  clsfval  23373  clsval  23385  clsval2  23398  hauscmplem  23754  cmpfi  23756  1stcfb  23793  fclscmp  24379  cutsval  28196  spanval  31965  chsupid  32044  intimafv  33375  fldgenval  33944  primefldgen1  33953  zarclsint  34574  zarcmplem  34583  sigagenval  34843  onvf1odlem3  36033  onprcf1acwevdlem2  36046  onvfowev  36050  onf1oracwevd  36052  kur14  36148  mclsval  36495  nmulprop  37117  nmulcom  37121  nmulrid  37124  igenval  39187  pclfvalN  41138  pclvalN  41139  diaintclN  42307  docaffvalN  42370  docafvalN  42371  docavalN  42372  dibintclN  42416  dihglb2  42591  dihintcl  42593  mzpval  43936  dnnumch3lem  44246  aomclem8  44256  rp-intrabeq  44415  nadd1suc  44586  minregex2  44728  salgenval  47536  mreclat  50316