Theorem rneq 5098

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 5049	. . 3 |- ( A = B -> `' A = `' B )
2	1	dmeqd 5075	. 2 |- ( A = B -> dom `' A = dom `' B )
3		df-rn 4892	. 2 |- ran A = dom `' A
4		df-rn 4892	. 2 |- ran B = dom `' B
5	2, 3, 4	3eqtr4g 2495	1 |- ( A = B -> ran A = ran B )

Syntax hints:   -> wi 4   = wceq 1653   `'ccnv 4880   dom cdm 4881   ran crn 4882

This theorem is referenced by:  rneqi  5099  rneqd  5100  feq1  5579  foeq1  5652  fnrnfv  5776  fconst5  5952  frxp  6459  tz7.44-2  6668  tz7.44-3  6669  map0e  7054  ixpsnf1o  7105  ordtypecbv  7489  ordtypelem3  7492  dfac8alem  7915  dfac8a  7916  dfac5lem3  8011  dfac9  8021  dfac12lem1  8028  dfac12r  8031  ackbij2  8128  isfin3ds  8214  fin23lem17  8223  fin23lem29  8226  fin23lem30  8227  fin23lem32  8229  fin23lem34  8231  fin23lem35  8232  fin23lem39  8235  fin23lem41  8237  isf33lem  8251  isf34lem6  8265  dcomex  8332  axdc2lem  8333  zorn2lem1  8381  zorn2g  8388  ttukey2g  8401  gruurn  8678  rpnnen1  10610  pnrmopn  17412  isi1f  19569  itg1val  19578  mpfrcl  19944  iscusgra  21470  isuvtx  21502  ex-rn  21753  gidval  21806  grpoinvfval  21817  grpodivfval  21835  gxfval  21850  isablo  21876  elghomlem1  21954  iscom2  22005  isdivrngo  22024  vci  22032  isvclem  22061  isnvlem  22094  isphg  22323  pj11i  23218  hmopidmch  23661  hmopidmpj  23662  pjss1coi  23671  issibf  24653  sitgfval  24660  ghomgrplem  25105  elgiso  25112  relexprn  25141  dfrtrcl2  25153  rdgprc0  25426  rdgprc  25427  dfrdg2  25428  brrangeg  25786  axlowdimlem13  25898  axlowdim1  25903  volsupnfl  26263  dnnumch1  27133  aomclem3  27145  aomclem8  27150  wwlk  28363  isfrgra  28454  csbima12gALTVD  29083

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419

This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2716  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-br 4216  df-opab 4270  df-cnv 4889  df-dm 4891  df-rn 4892