Theorem inteqd 4894

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

Syntax hints:   → wi 4   = wceq 1542  ∩ cint 4889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-ral 3052  df-rex 3062  df-int 4890

This theorem is referenced by:  elreldm  5890  ordintdif  6374  fniinfv  6918  onsucmin  7772  elxp5  7874  1stval2  7959  2ndval2  7960  naddcllem  8612  naddov2  8615  naddcom  8618  naddrid  8619  naddasslem1  8630  naddasslem2  8631  naddass  8632  naddsuc2  8637  fundmen  8978  xpsnen  8999  unblem2  9203  unblem3  9204  fiint  9237  elfi2  9327  fi0  9333  elfiun  9343  tcvalg  9657  tz9.12lem3  9713  rankvalb  9721  rankvalg  9741  ranksnb  9751  rankonidlem  9752  cardval3  9876  cardidm  9883  harsucnn  9922  cfval  10169  cflim3  10184  coftr  10195  isfin3ds  10251  fin23lem17  10260  fin23lem39  10272  isf33lem  10288  isf34lem5  10300  isf34lem6  10302  wuncval  10665  tskmval  10762  cleq1  14945  dfrtrcl2  15024  mrcfval  17574  mrcval  17576  cycsubg2  19185  efgval  19692  rgspnval  20589  lspfval  20968  lspval  20970  lsppropd  21013  aspval  21852  aspval2  21878  clsfval  22990  clsval  23002  clsval2  23015  hauscmplem  23371  cmpfi  23373  1stcfb  23410  fclscmp  23995  cutsval  27772  spanval  31404  chsupid  31483  intimafv  32784  fldgenval  33373  primefldgen1  33382  zarclsint  34016  zarcmplem  34025  sigagenval  34284  onvf1odlem3  35287  kur14  35398  mclsval  35745  igenval  38382  pclfvalN  40335  pclvalN  40336  diaintclN  41504  docaffvalN  41567  docafvalN  41568  docavalN  41569  dibintclN  41613  dihglb2  41788  dihintcl  41790  mzpval  43164  dnnumch3lem  43474  aomclem8  43489  rp-intrabeq  43649  nadd1suc  43820  minregex2  43962  iotain  44844  salgenval  46749  mreclat  49472