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 2796	1 ⊢ (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)

Syntax hints:   → wi 4   = wceq 1541  ^◡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 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  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  7152  frxp  8068  tz7.44-2  8338  tz7.44-3  8339  ixpsnf1o  8876  ordtypecbv  9422  ordtypelem3  9425  dfac8alem  9939  dfac8a  9940  dfac5lem3  10035  dfac9  10047  dfac12lem1  10054  dfac12r  10057  ackbij2  10152  isfin3ds  10239  fin23lem17  10248  fin23lem29  10251  fin23lem30  10252  fin23lem32  10254  fin23lem34  10256  fin23lem35  10257  fin23lem39  10260  fin23lem41  10262  isf33lem  10276  isf34lem6  10290  dcomex  10357  axdc2lem  10358  zorn2lem1  10406  zorn2g  10413  ttukey2g  10426  gruurn  10709  rpnnen1lem6  12895  relexp0g  14945  relexpsucnnr  14948  dfrtrcl2  14985  mpfrcl  22040  selvval  22078  ply1frcl  22262  pnrmopn  23287  isi1f  25631  itg1val  25640  madeval  27828  axlowdimlem13  29027  axlowdim1  29032  ausgrusgri  29241  0uhgrsubgr  29352  cusgrsize  29528  ex-rn  30515  gidval  30587  grpoinvfval  30597  grpodivfval  30609  isablo  30621  vciOLD  30636  isvclem  30652  isnvlem  30685  isphg  30892  pj11i  31786  hmopidmch  32228  hmopidmpj  32229  pjss1coi  32238  padct  32797  tocyc01  33200  tocyccntz  33226  unitprodclb  33470  esplyind  33731  locfinreflem  33997  locfinref  33998  issibf  34490  sitgfval  34498  onvf1odlem3  35299  mrsubvrs  35716  rdgprc0  35985  rdgprc  35986  dfrdg2  35987  brrangeg  36128  poimirlem24  37845  volsupnfl  37866  elghomlem1OLD  38086  isdivrngo  38151  iscom2  38196  elrefrels2  38771  elrefrels3  38772  refreleq  38774  elcnvrefrels2  38787  elcnvrefrels3  38788  dnnumch1  43286  aomclem3  43298  aomclem8  43303  rclexi  43856  rtrclex  43858  rtrclexi  43862  cnvrcl0  43866  dfrtrcl5  43870  dfrcl2  43915  csbima12gALTVD  45137  modelaxreplem1  45219  modelaxreplem2  45220  modelaxrep  45222  unirnmap  45452  ssmapsn  45460  sge0val  46610  vonvolmbl  46905