Theorem inteqi 2537

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 2536	. 2 |- (A = B -> |^|A = |^|B)
3	1, 2	ax-mp 7	1 |- |^|A = |^|B

Syntax hints:   = wceq 956  |^|cint 2533

This theorem is referenced by:  elintrab 2545  intmin2 2557  intsn 2564  intexrab 2732  intabs 2733  op1stb 2913  bm2.5ii 3019  op2ndb 3451  oawordeulem 4188  abfii1OLD 4561  abfii2OLD 4562  rankval2 4670  ranksn 4689  cf0 4910  dfnn2 5936

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-ral 1649  df-int 2534

Copyright terms: Public domain