Theorem rneq 5078

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 5026	. . 3 |- ( A = B -> `' A = `' B )
2	1	dmeqd 5055	. 2 |- ( A = B -> dom `' A = dom `' B )
3		df-rn 4863	. 2 |- ran A = dom `' A
4		df-rn 4863	. 2 |- ran B = dom `' B
5	2, 3, 4	3eqtr4g 2520	1 |- ( A = B -> ran A = ran B )

Syntax hints:   -> wi 4   = wceq 1454   `'ccnv 4851   dom cdm 4852   ran crn 4853

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-rab 2757  df-v 3058  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-if 3893  df-sn 3980  df-pr 3982  df-op 3986  df-br 4416  df-opab 4475  df-cnv 4860  df-dm 4862  df-rn 4863

This theorem is referenced by:  rneqi  5079  rneqd  5080  feq1  5731  foeq1  5811  fnrnfv  5933  fconst5  6145  frxp  6932  tz7.44-2  7150  tz7.44-3  7151  ixpsnf1o  7587  ordtypecbv  8057  ordtypelem3  8060  dfac8alem  8485  dfac8a  8486  dfac5lem3  8581  dfac9  8591  dfac12lem1  8598  dfac12r  8601  ackbij2  8698  isfin3ds  8784  fin23lem17  8793  fin23lem29  8796  fin23lem30  8797  fin23lem32  8799  fin23lem34  8801  fin23lem35  8802  fin23lem39  8805  fin23lem41  8807  isf33lem  8821  isf34lem6  8835  dcomex  8902  axdc2lem  8903  zorn2lem1  8951  zorn2g  8958  ttukey2g  8971  gruurn  9248  rpnnen1  11323  relexp0g  13133  relexpsucnnr  13136  dfrtrcl2  13173  mpfrcl  18789  ply1frcl  18955  pnrmopn  20407  isi1f  22680  itg1val  22689  axlowdimlem13  25032  axlowdim1  25037  iscusgra  25232  isuvtx  25264  wwlk  25457  clwwlk  25542  rusgra0edg  25731  isfrgra  25766  ex-rn  25938  gidval  25989  grpoinvfval  26000  grpodivfval  26018  gxfval  26033  isablo  26059  elghomlem1OLD  26137  iscom2  26188  isdivrngo  26207  vci  26215  isvclem  26244  isnvlem  26277  isphg  26506  pj11i  27412  hmopidmch  27854  hmopidmpj  27855  pjss1coi  27864  padct  28355  locfinreflem  28715  locfinref  28716  issibf  29214  sitgfval  29222  mrsubvrs  30208  ghomgrplem  30355  elgiso  30362  rdgprc0  30488  rdgprc  30489  dfrdg2  30490  brrangeg  30751  poimirlem24  32008  volsupnfl  32029  dnnumch1  35946  aomclem3  35958  aomclem8  35963  rclexi  36266  rtrclex  36268  rtrclexi  36272  cnvrcl0  36276  dfrtrcl5  36280  dfrcl2  36310  csbima12gALTVD  37333  sge0val  38245  ausgrusgri  39302  0uhgrsubgr  39400  cusgrsize  39564