Theorem inteqd 4912

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

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

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-ral 3078  df-rex 3088  df-int 4908

This theorem is used by:  elreldm  5917  ordintdif  6407  fniinfv  6955  onsucmin  7821  elxp5  7924  1stval2  8007  2ndval2  8008  naddcllem  8669  naddov2  8672  naddcom  8676  naddrid  8677  naddasslem1  8688  naddasslem2  8689  naddass  8690  naddsuc2  8695  fundmen  9043  xpsnen  9064  unblem2  9269  unblem3  9270  fiint  9302  elfi2  9390  fi0  9396  elfiun  9406  tcvalg  9721  tz9.12lem3  9779  rankvalb  9787  rankvalg  9807  ranksnb  9818  rankonidlem  9819  cardval3  10014  cardidm  10021  harsucnn  10060  cfval  10305  cflim3  10321  coftr  10332  isfin3ds  10388  fin23lem17  10397  fin23lem39  10409  isf33lem  10425  isf34lem5  10437  isf34lem6  10439  wuncval  10808  tskmval  10905  cleq1  15116  dfrtrcl2  15195  mrcfval  17762  mrcval  17764  cycsubg2  19405  efgval  19911  rgspnval  20844  lspfval  21228  lspval  21230  lsppropd  21273  rspvalint  21503  aspval  22160  aspval2  22186  clsfval  23323  clsval  23335  clsval2  23348  hauscmplem  23704  cmpfi  23706  1stcfb  23743  fclscmp  24329  cutsval  28148  spanval  31917  chsupid  31996  intimafv  33286  fldgenval  33856  primefldgen1  33865  zarclsint  34486  zarcmplem  34495  sigagenval  34755  onvf1odlem3  35857  onvfowev  35868  kur14  35950  mclsval  36297  nmulprop  36909  nmulcom  36913  nmulrid  36916  igenval  38963  pclfvalN  40914  pclvalN  40915  diaintclN  42083  docaffvalN  42146  docafvalN  42147  docavalN  42148  dibintclN  42192  dihglb2  42367  dihintcl  42369  mzpval  43696  dnnumch3lem  44006  aomclem8  44021  rp-intrabeq  44181  nadd1suc  44352  minregex2  44494  iotain  45360  salgenval  47275  mreclat  50049