Theorem rneq 5065

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 5013	. . 3 |- ( A = B -> `' A = `' B )
2	1	dmeqd 5042	. 2 |- ( A = B -> dom `' A = dom `' B )
3		df-rn 4851	. 2 |- ran A = dom `' A
4		df-rn 4851	. 2 |- ran B = dom `' B
5	2, 3, 4	3eqtr4g 2500	1 |- ( A = B -> ran A = ran B )

Syntax hints:   -> wi 4   = wceq 1369   `'ccnv 4839   dom cdm 4840   ran crn 4841

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-rab 2724  df-v 2974  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-sn 3878  df-pr 3880  df-op 3884  df-br 4293  df-opab 4351  df-cnv 4848  df-dm 4850  df-rn 4851

This theorem is referenced by:  rneqi  5066  rneqd  5067  feq1  5542  foeq1  5616  fnrnfv  5738  fconst5  5935  frxp  6682  tz7.44-2  6863  tz7.44-3  6864  map0e  7250  ixpsnf1o  7303  ordtypecbv  7731  ordtypelem3  7734  dfac8alem  8199  dfac8a  8200  dfac5lem3  8295  dfac9  8305  dfac12lem1  8312  dfac12r  8315  ackbij2  8412  isfin3ds  8498  fin23lem17  8507  fin23lem29  8510  fin23lem30  8511  fin23lem32  8513  fin23lem34  8515  fin23lem35  8516  fin23lem39  8519  fin23lem41  8521  isf33lem  8535  isf34lem6  8549  dcomex  8616  axdc2lem  8617  zorn2lem1  8665  zorn2g  8672  ttukey2g  8685  gruurn  8965  rpnnen1  10984  mpfrcl  17604  ply1frcl  17753  pnrmopn  18947  isi1f  21152  itg1val  21161  axlowdimlem13  23200  axlowdim1  23205  iscusgra  23364  isuvtx  23396  ex-rn  23647  gidval  23700  grpoinvfval  23711  grpodivfval  23729  gxfval  23744  isablo  23770  elghomlem1  23848  iscom2  23899  isdivrngo  23918  vci  23926  isvclem  23955  isnvlem  23988  isphg  24217  pj11i  25114  hmopidmch  25557  hmopidmpj  25558  pjss1coi  25567  issibf  26719  sitgfval  26727  ghomgrplem  27308  elgiso  27315  relexprn  27338  dfrtrcl2  27350  rdgprc0  27607  rdgprc  27608  dfrdg2  27609  brrangeg  27967  volsupnfl  28436  dnnumch1  29397  aomclem3  29409  aomclem8  29414  wwlk  30315  clwwlk  30429  rusgra0edg  30573  isfrgra  30582  csbima12gALTVD  31633