Theorem inteqd 2538

Description: Equality deduction for class intersection.

Hypothesis

Ref	Expression
inteqd.1	|- (ph -> A = B)

Assertion

Ref	Expression
inteqd	|- (ph -> |^|A = |^|B)

Proof of Theorem inteqd

Step	Hyp	Ref	Expression
1		inteqd.1	. 2 |- (ph -> A = B)
2		inteq 2536	. 2 |- (A = B -> |^|A = |^|B)
3	1, 2	syl 10	1 |- (ph -> |^|A = |^|B)

Syntax hints:   -> wi 3   = wceq 956  |^|cint 2533

This theorem is referenced by:  onsucmin 3072  elreldm 3338  elxp5 3454  fniinfv 3766  1stval2 4089  2ndval2 4090  fundmen 4428  xpsnen 4435  mapunen 4502  unblem2 4541  unblem3 4542  fiint 4559  fiintOLD 4560  tz9.12lem1 4659  tz9.12lem3 4661  rankval 4668  rankvalg 4669  rankonid 4695  oncardval 4819  cardval 4826  alephon 4865  alephsuc 4866  cfval 4906  xpnnen 7499  clsfval 7668  clsval 7677  spanvalt 9299  hsupval2t 9300  chsupid 9311  moec 10461  intprd 10471

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