Theorem inteqd 4907

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

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

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 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-ral 3052  df-rex 3061  df-int 4903

This theorem is referenced by:  elreldm  5884  ordintdif  6368  fniinfv  6912  onsucmin  7763  elxp5  7865  1stval2  7950  2ndval2  7951  naddcllem  8604  naddov2  8607  naddcom  8610  naddrid  8611  naddasslem1  8622  naddasslem2  8623  naddass  8624  naddsuc2  8629  fundmen  8968  xpsnen  8989  unblem2  9193  unblem3  9194  fiint  9227  elfi2  9317  fi0  9323  elfiun  9333  tcvalg  9645  tz9.12lem3  9701  rankvalb  9709  rankvalg  9729  ranksnb  9739  rankonidlem  9740  cardval3  9864  cardidm  9871  harsucnn  9910  cfval  10157  cflim3  10172  coftr  10183  isfin3ds  10239  fin23lem17  10248  fin23lem39  10260  isf33lem  10276  isf34lem5  10288  isf34lem6  10290  wuncval  10653  tskmval  10750  cleq1  14906  dfrtrcl2  14985  mrcfval  17531  mrcval  17533  cycsubg2  19139  efgval  19646  rgspnval  20545  lspfval  20924  lspval  20926  lsppropd  20970  aspval  21828  aspval2  21854  clsfval  22969  clsval  22981  clsval2  22994  hauscmplem  23350  cmpfi  23352  1stcfb  23389  fclscmp  23974  cutsval  27776  spanval  31408  chsupid  31487  intimafv  32790  fldgenval  33394  primefldgen1  33403  zarclsint  34029  zarcmplem  34038  sigagenval  34297  onvf1odlem3  35299  kur14  35410  mclsval  35757  igenval  38258  pclfvalN  40145  pclvalN  40146  diaintclN  41314  docaffvalN  41377  docafvalN  41378  docavalN  41379  dibintclN  41423  dihglb2  41598  dihintcl  41600  mzpval  42970  dnnumch3lem  43284  aomclem8  43299  rp-intrabeq  43459  nadd1suc  43630  minregex2  43772  iotain  44654  salgenval  46561  mreclat  49238