Theorem rneq 5782

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 5719	. . 3 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵)
2	1	dmeqd 5751	. 2 ⊢ (𝐴 = 𝐵 → dom ◡𝐴 = dom ◡𝐵)
3		df-rn 5539	. 2 ⊢ ran 𝐴 = dom ◡𝐴
4		df-rn 5539	. 2 ⊢ ran 𝐵 = dom ◡𝐵
5	2, 3, 4	3eqtr4g 2818	1 ⊢ (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)

Syntax hints:   → wi 4   = wceq 1538  ^◡ccnv 5527  dom cdm 5528  ran crn 5529

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-un 3865  df-in 3867  df-ss 3877  df-sn 4526  df-pr 4528  df-op 4532  df-br 5037  df-opab 5099  df-cnv 5536  df-dm 5538  df-rn 5539

This theorem is referenced by:  rneqi  5783  rneqd  5784  feq1  6484  foeq1  6577  fnrnfv  6718  fconst5  6965  frxp  7831  tz7.44-2  8059  tz7.44-3  8060  ixpsnf1o  8533  ordtypecbv  9027  ordtypelem3  9030  dfac8alem  9502  dfac8a  9503  dfac5lem3  9598  dfac9  9609  dfac12lem1  9616  dfac12r  9619  ackbij2  9716  isfin3ds  9802  fin23lem17  9811  fin23lem29  9814  fin23lem30  9815  fin23lem32  9817  fin23lem34  9819  fin23lem35  9820  fin23lem39  9823  fin23lem41  9825  isf33lem  9839  isf34lem6  9853  dcomex  9920  axdc2lem  9921  zorn2lem1  9969  zorn2g  9976  ttukey2g  9989  gruurn  10271  rpnnen1lem6  12435  relexp0g  14442  relexpsucnnr  14445  dfrtrcl2  14482  mpfrcl  20862  selvval  20895  ply1frcl  21051  pnrmopn  22057  isi1f  24388  itg1val  24397  axlowdimlem13  26861  axlowdim1  26866  ausgrusgri  27074  0uhgrsubgr  27182  cusgrsize  27357  ex-rn  28338  gidval  28408  grpoinvfval  28418  grpodivfval  28430  isablo  28442  vciOLD  28457  isvclem  28473  isnvlem  28506  isphg  28713  pj11i  29607  hmopidmch  30049  hmopidmpj  30050  pjss1coi  30059  padct  30591  tocyc01  30924  tocyccntz  30950  locfinreflem  31324  locfinref  31325  issibf  31832  sitgfval  31840  mrsubvrs  33013  rdgprc0  33298  rdgprc  33299  dfrdg2  33300  madeval  33631  brrangeg  33822  poimirlem24  35396  volsupnfl  35417  elghomlem1OLD  35638  isdivrngo  35703  iscom2  35748  elrefrels2  36232  elrefrels3  36233  refreleq  36235  elcnvrefrels2  36245  elcnvrefrels3  36246  dnnumch1  40406  aomclem3  40418  aomclem8  40423  rclexi  40733  rtrclex  40735  rtrclexi  40739  cnvrcl0  40743  dfrtrcl5  40747  dfrcl2  40793  csbima12gALTVD  42021  unirnmap  42252  ssmapsn  42260  sge0val  43416  vonvolmbl  43711