Theorem rneq 5936

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

Syntax hints:   → wi 4   = wceq 1542  ^◡ccnv 5676  dom cdm 5677  ran crn 5678

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-opab 5212  df-cnv 5685  df-dm 5687  df-rn 5688

This theorem is referenced by:  rneqi  5937  rneqd  5938  feq1  6699  foeq1  6802  fnrnfv  6952  fconst5  7207  frxp  8112  tz7.44-2  8407  tz7.44-3  8408  ixpsnf1o  8932  ordtypecbv  9512  ordtypelem3  9515  dfac8alem  10024  dfac8a  10025  dfac5lem3  10120  dfac9  10131  dfac12lem1  10138  dfac12r  10141  ackbij2  10238  isfin3ds  10324  fin23lem17  10333  fin23lem29  10336  fin23lem30  10337  fin23lem32  10339  fin23lem34  10341  fin23lem35  10342  fin23lem39  10345  fin23lem41  10347  isf33lem  10361  isf34lem6  10375  dcomex  10442  axdc2lem  10443  zorn2lem1  10491  zorn2g  10498  ttukey2g  10511  gruurn  10793  rpnnen1lem6  12966  relexp0g  14969  relexpsucnnr  14972  dfrtrcl2  15009  mpfrcl  21648  selvval  21681  ply1frcl  21837  pnrmopn  22847  isi1f  25191  itg1val  25200  madeval  27347  axlowdimlem13  28212  axlowdim1  28217  ausgrusgri  28428  0uhgrsubgr  28536  cusgrsize  28711  ex-rn  29693  gidval  29765  grpoinvfval  29775  grpodivfval  29787  isablo  29799  vciOLD  29814  isvclem  29830  isnvlem  29863  isphg  30070  pj11i  30964  hmopidmch  31406  hmopidmpj  31407  pjss1coi  31416  padct  31944  tocyc01  32277  tocyccntz  32303  locfinreflem  32820  locfinref  32821  issibf  33332  sitgfval  33340  mrsubvrs  34513  rdgprc0  34765  rdgprc  34766  dfrdg2  34767  brrangeg  34908  poimirlem24  36512  volsupnfl  36533  elghomlem1OLD  36753  isdivrngo  36818  iscom2  36863  elrefrels2  37388  elrefrels3  37389  refreleq  37391  elcnvrefrels2  37404  elcnvrefrels3  37405  dnnumch1  41786  aomclem3  41798  aomclem8  41803  rclexi  42366  rtrclex  42368  rtrclexi  42372  cnvrcl0  42376  dfrtrcl5  42380  dfrcl2  42425  csbima12gALTVD  43658  unirnmap  43907  ssmapsn  43915  sge0val  45082  vonvolmbl  45377