Theorem rneq 5885

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 5822	. . 3 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵)
2	1	dmeqd 5854	. 2 ⊢ (𝐴 = 𝐵 → dom ◡𝐴 = dom ◡𝐵)
3		df-rn 5635	. 2 ⊢ ran 𝐴 = dom ◡𝐴
4		df-rn 5635	. 2 ⊢ ran 𝐵 = dom ◡𝐵
5	2, 3, 4	3eqtr4g 2797	1 ⊢ (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)

Syntax hints:   → wi 4   = wceq 1542  ^◡ccnv 5623  dom cdm 5624  ran crn 5625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-cnv 5632  df-dm 5634  df-rn 5635

This theorem is referenced by:  rneqi  5886  rneqd  5887  feq1  6640  foeq1  6742  fnrnfv  6893  fconst5  7154  frxp  8069  tz7.44-2  8339  tz7.44-3  8340  ixpsnf1o  8879  ordtypecbv  9425  ordtypelem3  9428  dfac8alem  9942  dfac8a  9943  dfac5lem3  10038  dfac9  10050  dfac12lem1  10057  dfac12r  10060  ackbij2  10155  isfin3ds  10242  fin23lem17  10251  fin23lem29  10254  fin23lem30  10255  fin23lem32  10257  fin23lem34  10259  fin23lem35  10260  fin23lem39  10263  fin23lem41  10265  isf33lem  10279  isf34lem6  10293  dcomex  10360  axdc2lem  10361  zorn2lem1  10409  zorn2g  10416  ttukey2g  10429  gruurn  10712  rpnnen1lem6  12923  relexp0g  14975  relexpsucnnr  14978  dfrtrcl2  15015  mpfrcl  22073  selvval  22111  ply1frcl  22293  pnrmopn  23318  isi1f  25651  itg1val  25660  madeval  27838  axlowdimlem13  29037  axlowdim1  29042  ausgrusgri  29251  0uhgrsubgr  29362  cusgrsize  29538  ex-rn  30525  gidval  30598  grpoinvfval  30608  grpodivfval  30620  isablo  30632  vciOLD  30647  isvclem  30663  isnvlem  30696  isphg  30903  pj11i  31797  hmopidmch  32239  hmopidmpj  32240  pjss1coi  32249  padct  32806  tocyc01  33194  tocyccntz  33220  unitprodclb  33464  esplyfvaln  33733  esplyind  33734  locfinreflem  34000  locfinref  34001  issibf  34493  sitgfval  34501  onvf1odlem3  35303  mrsubvrs  35720  rdgprc0  35989  rdgprc  35990  dfrdg2  35991  brrangeg  36132  poimirlem24  37979  volsupnfl  38000  elghomlem1OLD  38220  isdivrngo  38285  iscom2  38330  elrefrels2  38933  elrefrels3  38934  refreleq  38936  elcnvrefrels2  38949  elcnvrefrels3  38950  dnnumch1  43490  aomclem3  43502  aomclem8  43507  rclexi  44060  rtrclex  44062  rtrclexi  44066  cnvrcl0  44070  dfrtrcl5  44074  dfrcl2  44119  csbima12gALTVD  45341  modelaxreplem1  45423  modelaxreplem2  45424  modelaxrep  45426  unirnmap  45655  ssmapsn  45663  sge0val  46812  vonvolmbl  47107