Theorem inteqi 2591

Description: Equality inference for class intersection.

Hypothesis

Ref	Expression
inteqi.1	|- A = B

Assertion

Ref	Expression
inteqi	|- |^|A = |^|B

Proof of Theorem inteqi

Step	Hyp	Ref	Expression
1		inteqi.1	. 2 |- A = B
2		inteq 2590	. 2 |- (A = B -> |^|A = |^|B)
3	1, 2	ax-mp 7	1 |- |^|A = |^|B

Syntax hints:   = wceq 997  |^|cint 2587

This theorem is referenced by:  elintrab 2599  intmin2 2611  intsn 2618  intexrab 2787  intabs 2788  op1stb 2970  bm2.5ii 3076  op2ndb 3508  oawordeulem 4246  abfii1 4621  abfii2 4622  rankval2 4732  ranksn 4751  cf0 4975  dfnn2 5996

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-10 1007  ax-12 1009  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504

This theorem depends on definitions:  df-bi 154  df-an 232  df-ex 1022  df-sb 1214  df-clab 1510  df-cleq 1515  df-clel 1518  df-ral 1696  df-int 2588

Copyright terms: Public domain