Theorem rneq 5228

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 5176	. . 3 |- ( A = B -> `' A = `' B )
2	1	dmeqd 5205	. 2 |- ( A = B -> dom `' A = dom `' B )
3		df-rn 5010	. 2 |- ran A = dom `' A
4		df-rn 5010	. 2 |- ran B = dom `' B
5	2, 3, 4	3eqtr4g 2533	1 |- ( A = B -> ran A = ran B )

Syntax hints:   -> wi 4   = wceq 1379   `'ccnv 4998   dom cdm 4999   ran crn 5000

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448  df-opab 4506  df-cnv 5007  df-dm 5009  df-rn 5010

This theorem is referenced by:  rneqi  5229  rneqd  5230  feq1  5713  foeq1  5791  fnrnfv  5914  fconst5  6118  frxp  6893  tz7.44-2  7073  tz7.44-3  7074  map0e  7456  ixpsnf1o  7509  ordtypecbv  7942  ordtypelem3  7945  dfac8alem  8410  dfac8a  8411  dfac5lem3  8506  dfac9  8516  dfac12lem1  8523  dfac12r  8526  ackbij2  8623  isfin3ds  8709  fin23lem17  8718  fin23lem29  8721  fin23lem30  8722  fin23lem32  8724  fin23lem34  8726  fin23lem35  8727  fin23lem39  8730  fin23lem41  8732  isf33lem  8746  isf34lem6  8760  dcomex  8827  axdc2lem  8828  zorn2lem1  8876  zorn2g  8883  ttukey2g  8896  gruurn  9176  rpnnen1  11213  mpfrcl  17986  ply1frcl  18154  pnrmopn  19638  isi1f  21844  itg1val  21853  axlowdimlem13  23961  axlowdim1  23966  iscusgra  24160  isuvtx  24192  wwlk  24385  clwwlk  24470  rusgra0edg  24659  isfrgra  24694  ex-rn  24866  gidval  24919  grpoinvfval  24930  grpodivfval  24948  gxfval  24963  isablo  24989  elghomlem1  25067  iscom2  25118  isdivrngo  25137  vci  25145  isvclem  25174  isnvlem  25207  isphg  25436  pj11i  26333  hmopidmch  26776  hmopidmpj  26777  pjss1coi  26786  issibf  27943  sitgfval  27951  ghomgrplem  28532  elgiso  28539  relexprn  28562  dfrtrcl2  28574  rdgprc0  28831  rdgprc  28832  dfrdg2  28833  brrangeg  29191  volsupnfl  29664  dnnumch1  30622  aomclem3  30634  aomclem8  30639  csbima12gALTVD  32795