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 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-ral 3079  df-rex 3089  df-int 4911

This theorem is used by:  elreldm  5923  ordintdif  6413  fniinfv  6960  onsucmin  7821  elxp5  7924  1stval2  8007  2ndval2  8008  naddcllem  8668  naddov2  8671  naddcom  8675  naddrid  8676  naddasslem1  8687  naddasslem2  8688  naddass  8689  naddsuc2  8694  fundmen  9042  xpsnen  9063  unblem2  9267  unblem3  9268  fiint  9300  elfi2  9388  fi0  9394  elfiun  9404  tcvalg  9719  tz9.12lem3  9775  rankvalb  9783  rankvalg  9803  ranksnb  9813  rankonidlem  9814  cardval3  9961  cardidm  9968  harsucnn  10007  cfval  10252  cflim3  10268  coftr  10279  isfin3ds  10335  fin23lem17  10344  fin23lem39  10356  isf33lem  10372  isf34lem5  10384  isf34lem6  10386  wuncval  10755  tskmval  10852  cleq1  15060  dfrtrcl2  15139  mrcfval  17702  mrcval  17704  cycsubg2  19344  efgval  19850  rgspnval  20780  lspfval  21163  lspval  21165  lsppropd  21208  rspvalint  21438  aspval  22093  aspval2  22119  clsfval  23256  clsval  23268  clsval2  23281  hauscmplem  23637  cmpfi  23639  1stcfb  23676  fclscmp  24262  cutsval  28053  spanval  31822  chsupid  31901  intimafv  33191  fldgenval  33761  primefldgen1  33770  zarclsint  34390  zarcmplem  34399  sigagenval  34659  onvf1odlem3  35710  onvfowev  35721  kur14  35803  mclsval  36150  nmulprop  36778  nmulcom  36782  nmulrid  36785  igenval  38819  pclfvalN  40770  pclvalN  40771  diaintclN  41939  docaffvalN  42002  docafvalN  42003  docavalN  42004  dibintclN  42048  dihglb2  42223  dihintcl  42225  mzpval  43585  dnnumch3lem  43895  aomclem8  43910  rp-intrabeq  44070  nadd1suc  44241  minregex2  44383  iotain  45249  salgenval  47157  mreclat  49931