Theorem inteqi 2532

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

Syntax hints:   = wceq 954  |^|cint 2528

This theorem is referenced by:  elintrab 2540  intmin2 2552  intsn 2559  intexrab 2727  intabs 2728  op1stb 2908  bm2.5ii 3014  op2ndb 3443  oawordeulem 4178  abfii1 4541  abfii2 4542  rankval2 4650  ranksn 4669  cf0 4890  dfnn2 5892

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-ral 1646  df-int 2529

Copyright terms: Public domain