Theorem inteqd 3219

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

Syntax hints:   -> wi 3   = wceq 1298  |^|cint 3214

This theorem is referenced by:  intprg 3251  onsucmin 3901  elreldm 4185  elxp5 4380  fniinfv 4727  1stval2 5030  2ndval2 5031  fundmen 5487  xpsnen 5494  mapunen 5596  unblem2 5634  unblem3 5635  fiint 5650  tz9.12lem1 5770  tz9.12lem3 5772  rankval 5779  rankvalg 5780  rankonid 5806  oncardval 5865  alephon 5876  omsubsuc 5877  cardval 5975  alephsuc 6014  cfval 6054  xpnnen 8768  clsfval 8944  clsval 8953  fbssint 10279  fbunfip 10282  spanval 10932  hsupval2 10933  chsupid 10944  moec 14351  istopx 14918  tarval2 15249  tarval2g 15250  fictb 15371  omsubsucOLD 15386  compfipin0lem 15435  compfipin0 15436  ist1-3 15543  fcluscomplem 15620  inficl 15757  heiborlem8 15962  heiborlem13 15967  igenval 16209  iotain 16381  ordintdif 16440

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-ral 2109  df-int 3215

Copyright terms: Public domain