Theorem inteqd 4902

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

Syntax hints:   → wi 4   = wceq 1541  ∩ cint 4897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-ral 3048  df-rex 3057  df-int 4898

This theorem is referenced by:  elreldm  5875  ordintdif  6357  fniinfv  6900  onsucmin  7751  elxp5  7853  1stval2  7938  2ndval2  7939  naddcllem  8591  naddov2  8594  naddcom  8597  naddrid  8598  naddasslem1  8609  naddasslem2  8610  naddass  8611  naddsuc2  8616  fundmen  8953  xpsnen  8974  unblem2  9177  unblem3  9178  fiint  9211  elfi2  9298  fi0  9304  elfiun  9314  tcvalg  9628  tz9.12lem3  9679  rankvalb  9687  rankvalg  9707  ranksnb  9717  rankonidlem  9718  cardval3  9842  cardidm  9849  harsucnn  9888  cfval  10135  cflim3  10150  coftr  10161  isfin3ds  10217  fin23lem17  10226  fin23lem39  10238  isf33lem  10254  isf34lem5  10266  isf34lem6  10268  wuncval  10630  tskmval  10727  cleq1  14887  dfrtrcl2  14966  mrcfval  17511  mrcval  17513  cycsubg2  19120  efgval  19627  rgspnval  20525  lspfval  20904  lspval  20906  lsppropd  20950  aspval  21808  aspval2  21833  clsfval  22938  clsval  22950  clsval2  22963  hauscmplem  23319  cmpfi  23321  1stcfb  23358  fclscmp  23943  scutval  27739  spanval  31308  chsupid  31387  intimafv  32687  fldgenval  33273  primefldgen1  33282  zarclsint  33880  zarcmplem  33889  sigagenval  34148  onvf1odlem3  35137  kur14  35248  mclsval  35595  igenval  38100  pclfvalN  39927  pclvalN  39928  diaintclN  41096  docaffvalN  41159  docafvalN  41160  docavalN  41161  dibintclN  41205  dihglb2  41380  dihintcl  41382  mzpval  42764  dnnumch3lem  43078  aomclem8  43093  rp-intrabeq  43253  nadd1suc  43424  minregex2  43567  iotain  44449  salgenval  46358  mreclat  49027