Theorem rneq 5893

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

Syntax hints:   → wi 4   = wceq 1542  ^◡ccnv 5631  dom cdm 5632  ran crn 5633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-cnv 5640  df-dm 5642  df-rn 5643

This theorem is referenced by:  rneqi  5894  rneqd  5895  feq1  6648  foeq1  6750  fnrnfv  6901  fconst5  7162  frxp  8078  tz7.44-2  8348  tz7.44-3  8349  ixpsnf1o  8888  ordtypecbv  9434  ordtypelem3  9437  dfac8alem  9951  dfac8a  9952  dfac5lem3  10047  dfac9  10059  dfac12lem1  10066  dfac12r  10069  ackbij2  10164  isfin3ds  10251  fin23lem17  10260  fin23lem29  10263  fin23lem30  10264  fin23lem32  10266  fin23lem34  10268  fin23lem35  10269  fin23lem39  10272  fin23lem41  10274  isf33lem  10288  isf34lem6  10302  dcomex  10369  axdc2lem  10370  zorn2lem1  10418  zorn2g  10425  ttukey2g  10438  gruurn  10721  rpnnen1lem6  12907  relexp0g  14957  relexpsucnnr  14960  dfrtrcl2  14997  mpfrcl  22052  selvval  22090  ply1frcl  22274  pnrmopn  23299  isi1f  25643  itg1val  25652  madeval  27840  axlowdimlem13  29039  axlowdim1  29044  ausgrusgri  29253  0uhgrsubgr  29364  cusgrsize  29540  ex-rn  30527  gidval  30599  grpoinvfval  30609  grpodivfval  30621  isablo  30633  vciOLD  30648  isvclem  30664  isnvlem  30697  isphg  30904  pj11i  31798  hmopidmch  32240  hmopidmpj  32241  pjss1coi  32250  padct  32807  tocyc01  33211  tocyccntz  33237  unitprodclb  33481  esplyfvaln  33750  esplyind  33751  locfinreflem  34017  locfinref  34018  issibf  34510  sitgfval  34518  onvf1odlem3  35318  mrsubvrs  35735  rdgprc0  36004  rdgprc  36005  dfrdg2  36006  brrangeg  36147  poimirlem24  37892  volsupnfl  37913  elghomlem1OLD  38133  isdivrngo  38198  iscom2  38243  elrefrels2  38846  elrefrels3  38847  refreleq  38849  elcnvrefrels2  38862  elcnvrefrels3  38863  dnnumch1  43398  aomclem3  43410  aomclem8  43415  rclexi  43968  rtrclex  43970  rtrclexi  43974  cnvrcl0  43978  dfrtrcl5  43982  dfrcl2  44027  csbima12gALTVD  45249  modelaxreplem1  45331  modelaxreplem2  45332  modelaxrep  45334  unirnmap  45563  ssmapsn  45571  sge0val  46721  vonvolmbl  47016