Theorem inteqd 4883

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

Syntax hints:   → wi 4   = wceq 1537  ∩ cint 4878

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-ral 3145  df-int 4879

This theorem is referenced by:  intprg  4912  elreldm  5807  ordintdif  6242  fniinfv  6744  onsucmin  7538  elxp5  7630  1stval2  7708  2ndval2  7709  fundmen  8585  xpsnen  8603  unblem2  8773  unblem3  8774  fiint  8797  elfi2  8880  fi0  8886  elfiun  8896  tcvalg  9182  tz9.12lem3  9220  rankvalb  9228  rankvalg  9248  ranksnb  9258  rankonidlem  9259  cardval3  9383  cardidm  9390  cfval  9671  cflim3  9686  coftr  9697  isfin3ds  9753  fin23lem17  9762  fin23lem39  9774  isf33lem  9790  isf34lem5  9802  isf34lem6  9804  wuncval  10166  tskmval  10263  cleq1  14345  dfrtrcl2  14423  mrcfval  16881  mrcval  16883  cycsubg2  18355  efgval  18845  lspfval  19747  lspval  19749  lsppropd  19792  aspval  20104  aspval2  20129  clsfval  21635  clsval  21647  clsval2  21660  hauscmplem  22016  cmpfi  22018  1stcfb  22055  fclscmp  22640  spanval  29112  chsupid  29191  sigagenval  31401  kur14  32465  mclsval  32812  scutval  33267  igenval  35341  pclfvalN  37027  pclvalN  37028  diaintclN  38196  docaffvalN  38259  docafvalN  38260  docavalN  38261  dibintclN  38305  dihglb2  38480  dihintcl  38482  mzpval  39336  dnnumch3lem  39653  aomclem8  39668  rgspnval  39775  harsucnn  39910  iotain  40756  salgenval  42613