Theorem rneq 5061

Description: Equality theorem for range. (Contributed by NM, 29-Dec-1996.)

Assertion

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

Proof of Theorem rneq

Step	Hyp	Ref	Expression
1		cnveq 5009	. . 3 |- ( A = B -> `' A = `' B )
2	1	dmeqd 5038	. 2 |- ( A = B -> dom `' A = dom `' B )
3		df-rn 4847	. 2 |- ran A = dom `' A
4		df-rn 4847	. 2 |- ran B = dom `' B
5	2, 3, 4	3eqtr4g 2498	1 |- ( A = B -> ran A = ran B )

Syntax hints:   -> wi 4   = wceq 1364   `'ccnv 4835   dom cdm 4836   ran crn 4837

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-rab 2722  df-v 2972  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-sn 3875  df-pr 3877  df-op 3881  df-br 4290  df-opab 4348  df-cnv 4844  df-dm 4846  df-rn 4847

This theorem is referenced by:  rneqi  5062  rneqd  5063  feq1  5539  foeq1  5613  fnrnfv  5735  fconst5  5932  frxp  6681  tz7.44-2  6859  tz7.44-3  6860  map0e  7246  ixpsnf1o  7299  ordtypecbv  7727  ordtypelem3  7730  dfac8alem  8195  dfac8a  8196  dfac5lem3  8291  dfac9  8301  dfac12lem1  8308  dfac12r  8311  ackbij2  8408  isfin3ds  8494  fin23lem17  8503  fin23lem29  8506  fin23lem30  8507  fin23lem32  8509  fin23lem34  8511  fin23lem35  8512  fin23lem39  8515  fin23lem41  8517  isf33lem  8531  isf34lem6  8545  dcomex  8612  axdc2lem  8613  zorn2lem1  8661  zorn2g  8668  ttukey2g  8681  gruurn  8961  rpnnen1  10980  pnrmopn  18847  isi1f  21052  itg1val  21061  mpfrcl  21428  axlowdimlem13  23119  axlowdim1  23124  iscusgra  23283  isuvtx  23315  ex-rn  23566  gidval  23619  grpoinvfval  23630  grpodivfval  23648  gxfval  23663  isablo  23689  elghomlem1  23767  iscom2  23818  isdivrngo  23837  vci  23845  isvclem  23874  isnvlem  23907  isphg  24136  pj11i  25033  hmopidmch  25476  hmopidmpj  25477  pjss1coi  25486  issibf  26633  sitgfval  26641  ghomgrplem  27221  elgiso  27228  relexprn  27251  dfrtrcl2  27263  rdgprc0  27520  rdgprc  27521  dfrdg2  27522  brrangeg  27880  volsupnfl  28345  dnnumch1  29306  aomclem3  29318  aomclem8  29323  wwlk  30224  clwwlk  30338  rusgra0edg  30482  isfrgra  30491  csbima12gALTVD  31450