Theorem rneq 5928

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

Syntax hints:   → wi 4   = wceq 1570  ^◡ccnv 5662  dom cdm 5663  ran crn 5664

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111  df-opab 5175  df-cnv 5671  df-dm 5673  df-rn 5674

This theorem is referenced by:  rneqi  5929  rneqd  5930  feq1  6685  foeq1  6790  fnrnfv  6942  fconst5  7206  frxp  8123  tz7.44-2  8395  tz7.44-3  8396  ixpsnf1o  8937  ordtypecbv  9480  ordtypelem3  9483  dfac8alem  10014  dfac8a  10015  dfac5lem3  10110  dfac9  10121  dfac12lem1  10128  dfac12r  10131  ackbij2  10226  isfin3ds  10314  fin23lem17  10323  fin23lem29  10326  fin23lem30  10327  fin23lem32  10329  fin23lem34  10331  fin23lem35  10332  fin23lem39  10335  fin23lem41  10337  isf33lem  10351  isf34lem6  10365  dcomex  10432  axdc2lem  10433  zorn2lem1  10481  zorn2g  10488  ttukey2g  10501  gruurn  10784  rpnnen1lem6  13007  relexp0g  15061  relexpsucnnr  15064  dfrtrcl2  15101  mpfrcl  22217  selvval  22252  ply1frcl  22459  pnrmopn  23481  isi1f  25814  itg1val  25823  madeval  28006  axlowdimlem13  29285  axlowdim1  29290  ausgrusgri  29499  0uhgrsubgr  29610  cusgrsize  29785  ex-rn  30772  gidval  30845  grpoinvfval  30855  grpodivfval  30867  isablo  30879  vciOLD  30894  isvclem  30910  isnvlem  30943  isphg  31150  pj11i  32044  hmopidmch  32486  hmopidmpj  32487  pjss1coi  32496  padct  33044  tocyc01  33419  tocyccntz  33445  unitprodclb  33683  esplyfvaln  33945  esplyind  33946  locfinreflem  34211  locfinref  34212  issibf  34704  sitgfval  34712  onvf1odlem3  35570  mrsubvrs  35995  rdgprc0  36264  rdgprc  36265  dfrdg2  36266  brrangeg  36407  poimirlem24  38276  volsupnfl  38297  elghomlem1OLD  38517  isdivrngo  38582  iscom2  38627  elrefrels2  39228  elrefrels3  39229  refreleq  39231  elcnvrefrels2  39244  elcnvrefrels3  39245  dnnumch1  43754  aomclem3  43766  aomclem8  43771  rclexi  44324  rtrclex  44326  rtrclexi  44330  cnvrcl0  44334  dfrtrcl5  44338  dfrcl2  44383  csbima12gALTVD  45588  modelaxreplem1  45670  modelaxreplem2  45671  modelaxrep  45673  unirnmap  45907  ssmapsn  45915  sge0val  47063  vonvolmbl  47358