Theorem rneq 5961

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 5898	. . 3 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵)
2	1	dmeqd 5930	. 2 ⊢ (𝐴 = 𝐵 → dom ◡𝐴 = dom ◡𝐵)
3		df-rn 5711	. 2 ⊢ ran 𝐴 = dom ◡𝐴
4		df-rn 5711	. 2 ⊢ ran 𝐵 = dom ◡𝐵
5	2, 3, 4	3eqtr4g 2805	1 ⊢ (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)

Syntax hints:   → wi 4   = wceq 1537  ^◡ccnv 5699  dom cdm 5700  ran crn 5701

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-opab 5229  df-cnv 5708  df-dm 5710  df-rn 5711

This theorem is referenced by:  rneqi  5962  rneqd  5963  feq1  6728  foeq1  6830  fnrnfv  6981  fconst5  7243  frxp  8167  tz7.44-2  8463  tz7.44-3  8464  ixpsnf1o  8996  ordtypecbv  9586  ordtypelem3  9589  dfac8alem  10098  dfac8a  10099  dfac5lem3  10194  dfac9  10206  dfac12lem1  10213  dfac12r  10216  ackbij2  10311  isfin3ds  10398  fin23lem17  10407  fin23lem29  10410  fin23lem30  10411  fin23lem32  10413  fin23lem34  10415  fin23lem35  10416  fin23lem39  10419  fin23lem41  10421  isf33lem  10435  isf34lem6  10449  dcomex  10516  axdc2lem  10517  zorn2lem1  10565  zorn2g  10572  ttukey2g  10585  gruurn  10867  rpnnen1lem6  13047  relexp0g  15071  relexpsucnnr  15074  dfrtrcl2  15111  mpfrcl  22132  selvval  22162  ply1frcl  22343  pnrmopn  23372  isi1f  25728  itg1val  25737  madeval  27909  axlowdimlem13  28987  axlowdim1  28992  ausgrusgri  29203  0uhgrsubgr  29314  cusgrsize  29490  ex-rn  30472  gidval  30544  grpoinvfval  30554  grpodivfval  30566  isablo  30578  vciOLD  30593  isvclem  30609  isnvlem  30642  isphg  30849  pj11i  31743  hmopidmch  32185  hmopidmpj  32186  pjss1coi  32195  padct  32733  tocyc01  33111  tocyccntz  33137  unitprodclb  33382  locfinreflem  33786  locfinref  33787  issibf  34298  sitgfval  34306  mrsubvrs  35490  rdgprc0  35757  rdgprc  35758  dfrdg2  35759  brrangeg  35900  poimirlem24  37604  volsupnfl  37625  elghomlem1OLD  37845  isdivrngo  37910  iscom2  37955  elrefrels2  38474  elrefrels3  38475  refreleq  38477  elcnvrefrels2  38490  elcnvrefrels3  38491  dnnumch1  43001  aomclem3  43013  aomclem8  43018  rclexi  43577  rtrclex  43579  rtrclexi  43583  cnvrcl0  43587  dfrtrcl5  43591  dfrcl2  43636  csbima12gALTVD  44868  unirnmap  45115  ssmapsn  45123  sge0val  46287  vonvolmbl  46582