Theorem rneq 5926

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 5859	. . 3 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵)
2	1	dmeqd 5895	. 2 ⊢ (𝐴 = 𝐵 → dom ◡𝐴 = dom ◡𝐵)
3		df-rn 5667	. 2 ⊢ ran 𝐴 = dom ◡𝐴
4		df-rn 5667	. 2 ⊢ ran 𝐵 = dom ◡𝐵
5	2, 3, 4	3eqtr4g 2823	1 ⊢ (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ^◡ccnv 5655  dom cdm 5656  ran crn 5657

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5172  df-cnv 5664  df-dm 5666  df-rn 5667

This theorem is used by:  rneqi  5927  rneqd  5928  feq1  6712  foeq1  6817  fnrnfv  6970  fconst5  7238  frxp  8168  tz7.44-2  8446  tz7.44-3  8447  ixpsnf1o  8997  ordtypecbv  9541  ordtypelem3  9544  dfac8alem  10138  dfac8a  10139  dfac5lem3  10234  dfac9  10245  dfac12lem1  10252  dfac12r  10255  ackbij2  10350  isfin3ds  10437  fin23lem17  10446  fin23lem29  10449  fin23lem30  10450  fin23lem32  10452  fin23lem34  10454  fin23lem35  10455  fin23lem39  10458  fin23lem41  10460  isf33lem  10474  isf34lem6  10488  dcomex  10555  axdc2lem  10556  zorn2lem1  10604  zorn2g  10611  ttukey2g  10624  gruurn  10913  rpnnen1lem6  13140  relexp0g  15207  relexpsucnnr  15210  dfrtrcl2  15247  mpfrcl  22427  selvval  22462  ply1frcl  22669  pnrmopn  23694  isi1f  26028  itg1val  26037  madeval  28251  axlowdimlem13  29565  axlowdim1  29570  ausgrusgri  29782  0uhgrsubgr  29893  cusgrsize  30068  ex-rn  31074  gidval  31147  grpoinvfval  31157  grpodivfval  31169  isablo  31181  vciOLD  31196  isvclem  31212  isnvlem  31245  isphg  31452  pj11i  32346  hmopidmch  32788  hmopidmpj  32789  pjss1coi  32798  padct  33384  tocyc01  33755  tocyccntz  33781  unitprodclb  34028  esplyfvaln  34289  esplyind  34290  locfinreflem  34555  locfinref  34556  issibf  35048  sitgfval  35056  fnlfvk30  36040  onvf1odlem3  36046  mrsubvrs  36467  rdgprc0  36746  rdgprc  36747  dfrdg2  36748  brrangeg  36889  poimirlem24  38767  volsupnfl  38788  elghomlem1OLD  39022  isdivrngo  39087  iscom2  39132  elrefrels2  39733  elrefrels3  39734  refreleq  39736  elcnvrefrels2  39749  elcnvrefrels3  39750  dnnumch1  44255  aomclem3  44262  aomclem8  44267  rclexi  44818  rtrclex  44820  rtrclexi  44824  cnvrcl0  44828  dfrtrcl5  44832  dfrcl2  44877  csbima12gALTVD  46081  modelaxreplem1  46174  modelaxreplem2  46175  modelaxrep  46177  unirnmap  46436  ssmapsn  46444  sge0val  47591  vonvolmbl  47886