Theorem rneq 3328

Description: Equality theorem for range.

Assertion

Ref	Expression
rneq	|- (A = B -> ran A = ran B)

Proof of Theorem rneq

Step	Hyp	Ref	Expression
1		cnveq 3281	. . 3 |- (A = B -> `'A = `'B)
2	1	dmeqd 3302	. 2 |- (A = B -> dom `' A = dom `' B)
3		df-rn 3179	. 2 |- ran A = dom `' A
4		df-rn 3179	. 2 |- ran B = dom `' B
5	2, 3, 4	3eqtr4g 1523	1 |- (A = B -> ran A = ran B)

Syntax hints:   -> wi 3   = wceq 953  `'ccnv 3159  dom cdm 3160  ran crn 3161

This theorem is referenced by:  rneqi 3329  rneqd 3330  feq1 3606  foeq1 3653  fvres 3719  fconst5 3833  tz7.44-3 3915  rdglem2 3923  map0e 4326  aceq5lem3 4709  numthlem 4755  numth 4756  zorn2lem1 4760  zorn2 4768  infxpidmlem4 7498  infxpidmlem8 7502  infxpidmlem10 7504  infmap2lem2 7522  bcth 7966  grpidval 7992  grpinvfval 8000  grpdivfval 8016  isabl 8037  isring 8078  ringi 8079  vci 8104  isvcgOLD 8133  isvclem 8134  isnvlem 8167  isnvgOLD 8168  nvi 8173  isphg 8407  pj11 9573  pjss1co 10002  elghomlem1 10287  ghomgrplem 10294  elgiso 10303  isalg 10497  algi 10504

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-sep 2693  ax-pow 2732  ax-pr 2769

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-v 1803  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-nul 2271  df-pw 2392  df-sn 2402  df-pr 2403  df-op 2406  df-br 2610  df-opab 2657  df-cnv 3176  df-dm 3178  df-rn 3179

Copyright terms: Public domain