Theorem inteqd 4902

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

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

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 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-ral 3049  df-rex 3058  df-int 4898

This theorem is referenced by:  elreldm  5879  ordintdif  6362  fniinfv  6906  onsucmin  7757  elxp5  7859  1stval2  7944  2ndval2  7945  naddcllem  8597  naddov2  8600  naddcom  8603  naddrid  8604  naddasslem1  8615  naddasslem2  8616  naddass  8617  naddsuc2  8622  fundmen  8960  xpsnen  8981  unblem2  9184  unblem3  9185  fiint  9218  elfi2  9305  fi0  9311  elfiun  9321  tcvalg  9633  tz9.12lem3  9689  rankvalb  9697  rankvalg  9717  ranksnb  9727  rankonidlem  9728  cardval3  9852  cardidm  9859  harsucnn  9898  cfval  10145  cflim3  10160  coftr  10171  isfin3ds  10227  fin23lem17  10236  fin23lem39  10248  isf33lem  10264  isf34lem5  10276  isf34lem6  10278  wuncval  10640  tskmval  10737  cleq1  14892  dfrtrcl2  14971  mrcfval  17516  mrcval  17518  cycsubg2  19124  efgval  19631  rgspnval  20529  lspfval  20908  lspval  20910  lsppropd  20954  aspval  21812  aspval2  21837  clsfval  22941  clsval  22953  clsval2  22966  hauscmplem  23322  cmpfi  23324  1stcfb  23361  fclscmp  23946  scutval  27742  spanval  31315  chsupid  31394  intimafv  32696  fldgenval  33285  primefldgen1  33294  zarclsint  33906  zarcmplem  33915  sigagenval  34174  onvf1odlem3  35170  kur14  35281  mclsval  35628  igenval  38121  pclfvalN  40008  pclvalN  40009  diaintclN  41177  docaffvalN  41240  docafvalN  41241  docavalN  41242  dibintclN  41286  dihglb2  41461  dihintcl  41463  mzpval  42849  dnnumch3lem  43163  aomclem8  43178  rp-intrabeq  43338  nadd1suc  43509  minregex2  43652  iotain  44534  salgenval  46443  mreclat  49121