Theorem rneq 4904

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 4855	. . 3 |- ( A = B -> `' A = `' B )
2	1	dmeqd 4881	. 2 |- ( A = B -> dom `' A = dom `' B )
3		df-rn 4700	. 2 |- ran A = dom `' A
4		df-rn 4700	. 2 |- ran B = dom `' B
5	2, 3, 4	3eqtr4g 2340	1 |- ( A = B -> ran A = ran B )

Syntax hints:   -> wi 4   = wceq 1623   `'ccnv 4688   dom cdm 4689   ran crn 4690

This theorem is referenced by:  rneqi  4905  rneqd  4906  feq1  5375  foeq1  5447  fnrnfv  5569  fconst5  5731  frxp  6225  tz7.44-2  6420  tz7.44-3  6421  map0e  6805  ixpsnf1o  6856  ordtypecbv  7232  ordtypelem3  7235  dfac8alem  7656  dfac8a  7657  dfac5lem3  7752  dfac9  7762  dfac12lem1  7769  dfac12r  7772  ackbij2  7869  isfin3ds  7955  fin23lem17  7964  fin23lem29  7967  fin23lem30  7968  fin23lem32  7970  fin23lem34  7972  fin23lem35  7973  fin23lem39  7976  fin23lem41  7978  isf33lem  7992  isf34lem6  8006  dcomex  8073  axdc2lem  8074  zorn2lem1  8123  zorn2g  8130  ttukey2g  8143  gruurn  8420  rpnnen1  10347  pnrmopn  17071  isi1f  19029  itg1val  19038  mpfrcl  19402  ex-rn  20827  gidval  20880  grpoinvfval  20891  grpodivfval  20909  gxfval  20924  isablo  20950  elghomlem1  21028  iscom2  21079  isdivrngo  21098  vci  21104  isvclem  21133  isnvlem  21166  isphg  21395  pj11i  22290  hmopidmch  22733  hmopidmpj  22734  pjss1coi  22743  ghomgrplem  23996  elgiso  24003  relexprn  24033  dfrtrcl2  24045  rdgprc0  24150  rdgprc  24151  dfrdg2  24152  brrangeg  24475  axlowdimlem13  24582  axlowdim1  24587  mgmrddd  25366  com2i  25416  rngodmeqrn  25419  vecval1b  25451  vecval3b  25452  vri  25492  isalg  25721  algi  25727  pfsubkl  26047  dnnumch1  27141  aomclem3  27153  aomclem8  27159  iscusgra  28153  isuvtx  28160  isfrgra  28171  csbima12gALTVD  28673

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024  df-opab 4078  df-cnv 4697  df-dm 4699  df-rn 4700