Theorem rneq 5918

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 5851	. . 3 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵)
2	1	dmeqd 5887	. 2 ⊢ (𝐴 = 𝐵 → dom ◡𝐴 = dom ◡𝐵)
3		df-rn 5662	. 2 ⊢ ran 𝐴 = dom ◡𝐴
4		df-rn 5662	. 2 ⊢ ran 𝐵 = dom ◡𝐵
5	2, 3, 4	3eqtr4g 2821	1 ⊢ (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ^◡ccnv 5650  dom cdm 5651  ran crn 5652

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-cnv 5659  df-dm 5661  df-rn 5662

This theorem is used by:  rneqi  5919  rneqd  5920  feq1  6679  foeq1  6784  fnrnfv  6936  fconst5  7204  frxp  8127  tz7.44-2  8399  tz7.44-3  8400  ixpsnf1o  8950  ordtypecbv  9495  ordtypelem3  9498  dfac8alem  10089  dfac8a  10090  dfac5lem3  10185  dfac9  10196  dfac12lem1  10203  dfac12r  10206  ackbij2  10301  isfin3ds  10388  fin23lem17  10397  fin23lem29  10400  fin23lem30  10401  fin23lem32  10403  fin23lem34  10405  fin23lem35  10406  fin23lem39  10409  fin23lem41  10411  isf33lem  10425  isf34lem6  10439  dcomex  10506  axdc2lem  10507  zorn2lem1  10555  zorn2g  10562  ttukey2g  10575  gruurn  10864  rpnnen1lem6  13091  relexp0g  15155  relexpsucnnr  15158  dfrtrcl2  15195  mpfrcl  22374  selvval  22409  ply1frcl  22616  pnrmopn  23641  isi1f  25975  itg1val  25984  madeval  28200  axlowdimlem13  29514  axlowdim1  29519  ausgrusgri  29731  0uhgrsubgr  29842  cusgrsize  30017  ex-rn  31023  gidval  31096  grpoinvfval  31106  grpodivfval  31118  isablo  31130  vciOLD  31145  isvclem  31161  isnvlem  31194  isphg  31401  pj11i  32295  hmopidmch  32737  hmopidmpj  32738  pjss1coi  32747  padct  33292  tocyc01  33661  tocyccntz  33687  unitprodclb  33926  esplyfvaln  34188  esplyind  34189  locfinreflem  34454  locfinref  34455  issibf  34948  sitgfval  34956  onvf1odlem3  35857  mrsubvrs  36256  rdgprc0  36525  rdgprc  36526  dfrdg2  36527  brrangeg  36668  poimirlem24  38530  volsupnfl  38551  elghomlem1OLD  38787  isdivrngo  38852  iscom2  38897  elrefrels2  39498  elrefrels3  39499  refreleq  39501  elcnvrefrels2  39514  elcnvrefrels3  39515  dnnumch1  44004  aomclem3  44016  aomclem8  44021  rclexi  44574  rtrclex  44576  rtrclexi  44580  cnvrcl0  44584  dfrtrcl5  44588  dfrcl2  44633  csbima12gALTVD  45838  modelaxreplem1  45920  modelaxreplem2  45921  modelaxrep  45923  unirnmap  46164  ssmapsn  46172  sge0val  47320  vonvolmbl  47615