Theorem inteqd 4445

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

Syntax hints:   → wi 4   = wceq 1480  ∩ cint 4440

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-int 4441

This theorem is referenced by:  intprg  4476  elreldm  5310  ordintdif  5733  fniinfv  6214  onsucmin  6968  elxp5  7058  1stval2  7130  2ndval2  7131  fundmen  7974  xpsnen  7988  unblem2  8157  unblem3  8158  fiint  8181  elfi2  8264  fi0  8270  elfiun  8280  tcvalg  8558  tz9.12lem3  8596  rankvalb  8604  rankvalg  8624  ranksnb  8634  rankonidlem  8635  cardval3  8722  cardidm  8729  cfval  9013  cflim3  9028  coftr  9039  isfin3ds  9095  fin23lem17  9104  fin23lem39  9116  isf33lem  9132  isf34lem5  9144  isf34lem6  9146  wuncval  9508  tskmval  9605  cleq1  13656  dfrtrcl2  13736  mrcfval  16189  mrcval  16191  cycsubg2  17552  efgval  18051  lspfval  18892  lspval  18894  lsppropd  18937  aspval  19247  aspval2  19266  clsfval  20739  clsval  20751  clsval2  20764  hauscmplem  21119  cmpfi  21121  1stcfb  21158  fclscmp  21744  spanval  28041  chsupid  28120  sigagenval  29984  kur14  30906  mclsval  31168  igenval  33492  pclfvalN  34655  pclvalN  34656  diaintclN  35827  docaffvalN  35890  docafvalN  35891  docavalN  35892  dibintclN  35936  dihglb2  36111  dihintcl  36113  mzpval  36775  dnnumch3lem  37096  aomclem8  37111  rgspnval  37219  iotain  38100  salgenval  39848