Theorem inteqd 4975

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

Syntax hints:   → wi 4   = wceq 1537  ∩ cint 4970

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-ral 3068  df-rex 3077  df-int 4971

This theorem is referenced by:  elreldm  5960  ordintdif  6445  fniinfv  7000  onsucmin  7857  elxp5  7963  1stval2  8047  2ndval2  8048  naddcllem  8732  naddov2  8735  naddcom  8738  naddrid  8739  naddasslem1  8750  naddasslem2  8751  naddass  8752  naddsuc2  8757  fundmen  9096  xpsnen  9121  unblem2  9357  unblem3  9358  fiint  9394  fiintOLD  9395  elfi2  9483  fi0  9489  elfiun  9499  tcvalg  9807  tz9.12lem3  9858  rankvalb  9866  rankvalg  9886  ranksnb  9896  rankonidlem  9897  cardval3  10021  cardidm  10028  harsucnn  10067  cfval  10316  cflim3  10331  coftr  10342  isfin3ds  10398  fin23lem17  10407  fin23lem39  10419  isf33lem  10435  isf34lem5  10447  isf34lem6  10449  wuncval  10811  tskmval  10908  cleq1  15032  dfrtrcl2  15111  mrcfval  17666  mrcval  17668  cycsubg2  19250  efgval  19759  lspfval  20994  lspval  20996  lsppropd  21040  aspval  21916  aspval2  21941  clsfval  23054  clsval  23066  clsval2  23079  hauscmplem  23435  cmpfi  23437  1stcfb  23474  fclscmp  24059  scutval  27863  spanval  31365  chsupid  31444  intimafv  32722  fldgenval  33279  primefldgen1  33288  zarclsint  33818  zarcmplem  33827  sigagenval  34104  kur14  35184  mclsval  35531  igenval  38021  pclfvalN  39846  pclvalN  39847  diaintclN  41015  docaffvalN  41078  docafvalN  41079  docavalN  41080  dibintclN  41124  dihglb2  41299  dihintcl  41301  mzpval  42688  dnnumch3lem  43003  aomclem8  43018  rgspnval  43125  rp-intrabeq  43182  nadd1suc  43354  minregex2  43497  iotain  44386  salgenval  46242  mreclat  48669