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

Syntax hints:   → wi 4   = wceq 1547  ^◡ccnv 5624  dom cdm 5625  ran crn 5626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080  df-opab 5142  df-cnv 5633  df-dm 5635  df-rn 5636

This theorem is referenced by:  rneqi  5886  rneqd  5887  feq1  6640  foeq1  6742  fnrnfv  6893  fconst5  7157  frxp  8073  tz7.44-2  8343  tz7.44-3  8344  ixpsnf1o  8883  ordtypecbv  9429  ordtypelem3  9432  dfac8alem  9949  dfac8a  9950  dfac5lem3  10045  dfac9  10057  dfac12lem1  10064  dfac12r  10067  ackbij2  10162  isfin3ds  10249  fin23lem17  10258  fin23lem29  10261  fin23lem30  10262  fin23lem32  10264  fin23lem34  10266  fin23lem35  10267  fin23lem39  10270  fin23lem41  10272  isf33lem  10286  isf34lem6  10300  dcomex  10367  axdc2lem  10368  zorn2lem1  10416  zorn2g  10423  ttukey2g  10436  gruurn  10719  rpnnen1lem6  12930  relexp0g  14982  relexpsucnnr  14985  dfrtrcl2  15022  mpfrcl  22068  selvval  22103  ply1frcl  22311  pnrmopn  23333  isi1f  25666  itg1val  25675  madeval  27849  axlowdimlem13  29048  axlowdim1  29053  ausgrusgri  29262  0uhgrsubgr  29373  cusgrsize  29548  ex-rn  30535  gidval  30608  grpoinvfval  30618  grpodivfval  30630  isablo  30642  vciOLD  30657  isvclem  30673  isnvlem  30706  isphg  30913  pj11i  31807  hmopidmch  32249  hmopidmpj  32250  pjss1coi  32259  padct  32817  tocyc01  33206  tocyccntz  33232  unitprodclb  33479  esplyfvaln  33765  esplyind  33766  locfinreflem  34031  locfinref  34032  issibf  34524  sitgfval  34532  onvf1odlem3  35340  mrsubvrs  35757  rdgprc0  36026  rdgprc  36027  dfrdg2  36028  brrangeg  36169  poimirlem24  38018  volsupnfl  38039  elghomlem1OLD  38259  isdivrngo  38324  iscom2  38369  elrefrels2  38972  elrefrels3  38973  refreleq  38975  elcnvrefrels2  38988  elcnvrefrels3  38989  dnnumch1  43496  aomclem3  43508  aomclem8  43513  rclexi  44066  rtrclex  44068  rtrclexi  44072  cnvrcl0  44076  dfrtrcl5  44080  dfrcl2  44125  csbima12gALTVD  45347  modelaxreplem1  45429  modelaxreplem2  45430  modelaxrep  45432  unirnmap  45660  ssmapsn  45668  sge0val  46816  vonvolmbl  47111