Theorem rneq 5054

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 5005	. . 3 |- ( A = B -> `' A = `' B )
2	1	dmeqd 5031	. 2 |- ( A = B -> dom `' A = dom `' B )
3		df-rn 4848	. 2 |- ran A = dom `' A
4		df-rn 4848	. 2 |- ran B = dom `' B
5	2, 3, 4	3eqtr4g 2461	1 |- ( A = B -> ran A = ran B )

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

This theorem is referenced by:  rneqi  5055  rneqd  5056  feq1  5535  foeq1  5608  fnrnfv  5732  fconst5  5908  frxp  6415  tz7.44-2  6624  tz7.44-3  6625  map0e  7010  ixpsnf1o  7061  ordtypecbv  7442  ordtypelem3  7445  dfac8alem  7866  dfac8a  7867  dfac5lem3  7962  dfac9  7972  dfac12lem1  7979  dfac12r  7982  ackbij2  8079  isfin3ds  8165  fin23lem17  8174  fin23lem29  8177  fin23lem30  8178  fin23lem32  8180  fin23lem34  8182  fin23lem35  8183  fin23lem39  8186  fin23lem41  8188  isf33lem  8202  isf34lem6  8216  dcomex  8283  axdc2lem  8284  zorn2lem1  8332  zorn2g  8339  ttukey2g  8352  gruurn  8629  rpnnen1  10561  pnrmopn  17361  isi1f  19519  itg1val  19528  mpfrcl  19892  iscusgra  21418  isuvtx  21450  ex-rn  21701  gidval  21754  grpoinvfval  21765  grpodivfval  21783  gxfval  21798  isablo  21824  elghomlem1  21902  iscom2  21953  isdivrngo  21972  vci  21980  isvclem  22009  isnvlem  22042  isphg  22271  pj11i  23166  hmopidmch  23609  hmopidmpj  23610  pjss1coi  23619  issibf  24601  sitgfval  24608  ghomgrplem  25053  elgiso  25060  relexprn  25089  dfrtrcl2  25101  rdgprc0  25364  rdgprc  25365  dfrdg2  25366  brrangeg  25689  axlowdimlem13  25797  axlowdim1  25802  volsupnfl  26150  dnnumch1  27009  aomclem3  27021  aomclem8  27027  isfrgra  28094  csbima12gALTVD  28718

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-br 4173  df-opab 4227  df-cnv 4845  df-dm 4847  df-rn 4848