Theorem rneq 5834

Description: Equality theorem for range. (Contributed by NM, 29-Dec-1996.)

Assertion

Ref	Expression
rneq	⊢ (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)

Proof of Theorem rneq

Step	Hyp	Ref	Expression
1		cnveq 5771	. . 3 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵)
2	1	dmeqd 5803	. 2 ⊢ (𝐴 = 𝐵 → dom ◡𝐴 = dom ◡𝐵)
3		df-rn 5591	. 2 ⊢ ran 𝐴 = dom ◡𝐴
4		df-rn 5591	. 2 ⊢ ran 𝐵 = dom ◡𝐵
5	2, 3, 4	3eqtr4g 2804	1 ⊢ (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)

Syntax hints:   → wi 4   = wceq 1539  ^◡ccnv 5579  dom cdm 5580  ran crn 5581

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-cnv 5588  df-dm 5590  df-rn 5591

This theorem is referenced by:  rneqi  5835  rneqd  5836  feq1  6565  foeq1  6668  fnrnfv  6811  fconst5  7063  frxp  7938  tz7.44-2  8209  tz7.44-3  8210  ixpsnf1o  8684  ordtypecbv  9206  ordtypelem3  9209  dfac8alem  9716  dfac8a  9717  dfac5lem3  9812  dfac9  9823  dfac12lem1  9830  dfac12r  9833  ackbij2  9930  isfin3ds  10016  fin23lem17  10025  fin23lem29  10028  fin23lem30  10029  fin23lem32  10031  fin23lem34  10033  fin23lem35  10034  fin23lem39  10037  fin23lem41  10039  isf33lem  10053  isf34lem6  10067  dcomex  10134  axdc2lem  10135  zorn2lem1  10183  zorn2g  10190  ttukey2g  10203  gruurn  10485  rpnnen1lem6  12651  relexp0g  14661  relexpsucnnr  14664  dfrtrcl2  14701  mpfrcl  21205  selvval  21238  ply1frcl  21394  pnrmopn  22402  isi1f  24743  itg1val  24752  axlowdimlem13  27225  axlowdim1  27230  ausgrusgri  27441  0uhgrsubgr  27549  cusgrsize  27724  ex-rn  28705  gidval  28775  grpoinvfval  28785  grpodivfval  28797  isablo  28809  vciOLD  28824  isvclem  28840  isnvlem  28873  isphg  29080  pj11i  29974  hmopidmch  30416  hmopidmpj  30417  pjss1coi  30426  padct  30956  tocyc01  31287  tocyccntz  31313  locfinreflem  31692  locfinref  31693  issibf  32200  sitgfval  32208  mrsubvrs  33384  rdgprc0  33675  rdgprc  33676  dfrdg2  33677  madeval  33963  brrangeg  34165  poimirlem24  35728  volsupnfl  35749  elghomlem1OLD  35970  isdivrngo  36035  iscom2  36080  elrefrels2  36562  elrefrels3  36563  refreleq  36565  elcnvrefrels2  36575  elcnvrefrels3  36576  dnnumch1  40785  aomclem3  40797  aomclem8  40802  rclexi  41112  rtrclex  41114  rtrclexi  41118  cnvrcl0  41122  dfrtrcl5  41126  dfrcl2  41171  csbima12gALTVD  42406  unirnmap  42637  ssmapsn  42645  sge0val  43794  vonvolmbl  44089