Theorem rneq 5900

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 5837	. . 3 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵)
2	1	dmeqd 5869	. 2 ⊢ (𝐴 = 𝐵 → dom ◡𝐴 = dom ◡𝐵)
3		df-rn 5649	. 2 ⊢ ran 𝐴 = dom ◡𝐴
4		df-rn 5649	. 2 ⊢ ran 𝐵 = dom ◡𝐵
5	2, 3, 4	3eqtr4g 2789	1 ⊢ (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)

Syntax hints:   → wi 4   = wceq 1540  ^◡ccnv 5637  dom cdm 5638  ran crn 5639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-cnv 5646  df-dm 5648  df-rn 5649

This theorem is referenced by:  rneqi  5901  rneqd  5902  feq1  6666  foeq1  6768  fnrnfv  6920  fconst5  7180  frxp  8105  tz7.44-2  8375  tz7.44-3  8376  ixpsnf1o  8911  ordtypecbv  9470  ordtypelem3  9473  dfac8alem  9982  dfac8a  9983  dfac5lem3  10078  dfac9  10090  dfac12lem1  10097  dfac12r  10100  ackbij2  10195  isfin3ds  10282  fin23lem17  10291  fin23lem29  10294  fin23lem30  10295  fin23lem32  10297  fin23lem34  10299  fin23lem35  10300  fin23lem39  10303  fin23lem41  10305  isf33lem  10319  isf34lem6  10333  dcomex  10400  axdc2lem  10401  zorn2lem1  10449  zorn2g  10456  ttukey2g  10469  gruurn  10751  rpnnen1lem6  12941  relexp0g  14988  relexpsucnnr  14991  dfrtrcl2  15028  mpfrcl  21992  selvval  22022  ply1frcl  22205  pnrmopn  23230  isi1f  25575  itg1val  25584  madeval  27760  axlowdimlem13  28881  axlowdim1  28886  ausgrusgri  29095  0uhgrsubgr  29206  cusgrsize  29382  ex-rn  30369  gidval  30441  grpoinvfval  30451  grpodivfval  30463  isablo  30475  vciOLD  30490  isvclem  30506  isnvlem  30539  isphg  30746  pj11i  31640  hmopidmch  32082  hmopidmpj  32083  pjss1coi  32092  padct  32643  tocyc01  33075  tocyccntz  33101  unitprodclb  33360  locfinreflem  33830  locfinref  33831  issibf  34324  sitgfval  34332  onvf1odlem3  35092  mrsubvrs  35509  rdgprc0  35781  rdgprc  35782  dfrdg2  35783  brrangeg  35924  poimirlem24  37638  volsupnfl  37659  elghomlem1OLD  37879  isdivrngo  37944  iscom2  37989  elrefrels2  38509  elrefrels3  38510  refreleq  38512  elcnvrefrels2  38525  elcnvrefrels3  38526  dnnumch1  43033  aomclem3  43045  aomclem8  43050  rclexi  43604  rtrclex  43606  rtrclexi  43610  cnvrcl0  43614  dfrtrcl5  43618  dfrcl2  43663  csbima12gALTVD  44886  modelaxreplem1  44968  modelaxreplem2  44969  modelaxrep  44971  unirnmap  45202  ssmapsn  45210  sge0val  46364  vonvolmbl  46659