Theorem inteqi 4888

Description: Equality inference for class intersection. (Contributed by NM, 2-Sep-2003.)

Hypothesis

Ref	Expression
inteqi.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
inteqi	⊢ ∩ 𝐴 = ∩ 𝐵

Proof of Theorem inteqi

Step	Hyp	Ref	Expression
1		inteqi.1	. 2 ⊢ 𝐴 = 𝐵
2		inteq 4887	. 2 ⊢ (𝐴 = 𝐵 → ∩ 𝐴 = ∩ 𝐵)
3	1, 2	ax-mp 5	1 ⊢ ∩ 𝐴 = ∩ 𝐵

Syntax hints:   = wceq 1547  ∩ cint 4884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-ral 3055  df-rex 3065  df-int 4885

This theorem is referenced by:  elintrab  4897  ssintrab  4908  intmin2  4912  intsng  4920  intexrab  5282  intabs  5284  op1stb  5418  dfiin3g  5918  op2ndb  6185  ordintdif  6368  knatar  7308  uniordint  7751  oawordeulem  8486  oeeulem  8534  naddov3  8613  iinfi  9327  dfttrcl2  9643  tcsni  9660  rankval2  9740  rankval3b  9748  cf0  10171  cfval2  10180  cofsmo  10189  isf34lem4  10297  isf34lem7  10299  sstskm  10763  dfnn3  12186  trclun  14974  cycsubg  19181  efgval2  19697  00lsp  20978  alexsublem  24034  noextendlt  27658  nosepne  27669  nosepdm  27673  nosupbnd2lem1  27704  noinfbnd2lem1  27719  noetasuplem4  27725  bday0  27828  intimafv  32810  dynkin  34358  rankval2b  35287  tz9.1regs  35322  imaiinfv  43149  elrfi  43150  onuniintrab  43678  naddov4  43835  naddwordnexlem4  43853  harval3  43989  relintab  44034  dfid7  44063  clcnvlem  44074  dfrtrcl5  44080  dfrcl2  44125  aiotajust  47554  dfaiota2  47556  ipolub0  49489