Theorem inteqd 2542

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 2540	. 2 |- (A = B -> |^|A = |^|B)
3	1, 2	syl 10	1 |- (ph -> |^|A = |^|B)

Syntax hints:   -> wi 3   = wceq 958  |^|cint 2537

This theorem is referenced by:  onsucmin 3078  elreldm 3344  elxp5 3460  fniinfv 3772  1stval2 4095  2ndval2 4096  fundmen 4434  xpsnen 4441  mapunen 4508  unblem2 4552  unblem3 4553  fiint 4572  fiintOLD 4573  tz9.12lem1 4669  tz9.12lem3 4671  rankval 4678  rankvalg 4679  rankonid 4705  oncardval 4829  cardval 4836  alephon 4876  alephsuc 4877  cfval 4918  xpnnen 7500  clsfval 7665  clsval 7674  spanvalt 9294  hsupval2t 9295  chsupid 9306  moec 10451  intprd 10461

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-ral 1652  df-int 2538

Copyright terms: Public domain