Theorem rneq 5917

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 5850	. . 3 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵)
2	1	dmeqd 5886	. 2 ⊢ (𝐴 = 𝐵 → dom ◡𝐴 = dom ◡𝐵)
3		df-rn 5663	. 2 ⊢ ran 𝐴 = dom ◡𝐴
4		df-rn 5663	. 2 ⊢ ran 𝐵 = dom ◡𝐵
5	2, 3, 4	3eqtr4g 2825	1 ⊢ (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)

Syntax hints:   → wi 4   = wceq 1563  ^◡ccnv 5651  dom cdm 5652  ran crn 5653

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-br 5106  df-opab 5168  df-cnv 5660  df-dm 5662  df-rn 5663

This theorem is referenced by:  rneqi  5918  rneqd  5919  feq1  6673  foeq1  6778  fnrnfv  6930  fconst5  7194  frxp  8110  tz7.44-2  8382  tz7.44-3  8383  ixpsnf1o  8924  ordtypecbv  9467  ordtypelem3  9470  dfac8alem  10001  dfac8a  10002  dfac5lem3  10097  dfac9  10108  dfac12lem1  10115  dfac12r  10118  ackbij2  10213  isfin3ds  10301  fin23lem17  10310  fin23lem29  10313  fin23lem30  10314  fin23lem32  10316  fin23lem34  10318  fin23lem35  10319  fin23lem39  10322  fin23lem41  10324  isf33lem  10338  isf34lem6  10352  dcomex  10419  axdc2lem  10420  zorn2lem1  10468  zorn2g  10475  ttukey2g  10488  gruurn  10771  rpnnen1lem6  12997  relexp0g  15049  relexpsucnnr  15052  dfrtrcl2  15089  mpfrcl  22196  selvval  22231  ply1frcl  22439  pnrmopn  23461  isi1f  25794  itg1val  25803  madeval  27983  axlowdimlem13  29213  axlowdim1  29218  ausgrusgri  29427  0uhgrsubgr  29538  cusgrsize  29713  ex-rn  30700  gidval  30773  grpoinvfval  30783  grpodivfval  30795  isablo  30807  vciOLD  30822  isvclem  30838  isnvlem  30871  isphg  31078  pj11i  31972  hmopidmch  32414  hmopidmpj  32415  pjss1coi  32424  padct  32975  tocyc01  33351  tocyccntz  33377  unitprodclb  33618  esplyfvaln  33881  esplyind  33882  locfinreflem  34147  locfinref  34148  issibf  34640  sitgfval  34648  onvf1odlem3  35460  mrsubvrs  35885  rdgprc0  36154  rdgprc  36155  dfrdg2  36156  brrangeg  36297  poimirlem24  38155  volsupnfl  38176  elghomlem1OLD  38396  isdivrngo  38461  iscom2  38506  elrefrels2  39109  elrefrels3  39110  refreleq  39112  elcnvrefrels2  39125  elcnvrefrels3  39126  dnnumch1  43633  aomclem3  43645  aomclem8  43650  rclexi  44203  rtrclex  44205  rtrclexi  44209  cnvrcl0  44213  dfrtrcl5  44217  dfrcl2  44262  csbima12gALTVD  45470  modelaxreplem1  45552  modelaxreplem2  45553  modelaxrep  45555  unirnmap  45782  ssmapsn  45790  sge0val  46938  vonvolmbl  47233