Theorem rneq 5929

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

Syntax hints:   → wi 4   = wceq 1533  ^◡ccnv 5668  dom cdm 5669  ran crn 5670

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2704  df-cleq 2718  df-clel 2804  df-rab 3427  df-v 3470  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-nul 4318  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-br 5142  df-opab 5204  df-cnv 5677  df-dm 5679  df-rn 5680

This theorem is referenced by:  rneqi  5930  rneqd  5931  feq1  6692  foeq1  6795  fnrnfv  6945  fconst5  7203  frxp  8112  tz7.44-2  8408  tz7.44-3  8409  ixpsnf1o  8934  ordtypecbv  9514  ordtypelem3  9517  dfac8alem  10026  dfac8a  10027  dfac5lem3  10122  dfac9  10133  dfac12lem1  10140  dfac12r  10143  ackbij2  10240  isfin3ds  10326  fin23lem17  10335  fin23lem29  10338  fin23lem30  10339  fin23lem32  10341  fin23lem34  10343  fin23lem35  10344  fin23lem39  10347  fin23lem41  10349  isf33lem  10363  isf34lem6  10377  dcomex  10444  axdc2lem  10445  zorn2lem1  10493  zorn2g  10500  ttukey2g  10513  gruurn  10795  rpnnen1lem6  12970  relexp0g  14975  relexpsucnnr  14978  dfrtrcl2  15015  mpfrcl  21990  selvval  22020  ply1frcl  22192  pnrmopn  23202  isi1f  25558  itg1val  25567  madeval  27734  axlowdimlem13  28720  axlowdim1  28725  ausgrusgri  28936  0uhgrsubgr  29044  cusgrsize  29220  ex-rn  30202  gidval  30274  grpoinvfval  30284  grpodivfval  30296  isablo  30308  vciOLD  30323  isvclem  30339  isnvlem  30372  isphg  30579  pj11i  31473  hmopidmch  31915  hmopidmpj  31916  pjss1coi  31925  padct  32451  tocyc01  32783  tocyccntz  32809  locfinreflem  33350  locfinref  33351  issibf  33862  sitgfval  33870  mrsubvrs  35041  rdgprc0  35298  rdgprc  35299  dfrdg2  35300  brrangeg  35441  poimirlem24  37025  volsupnfl  37046  elghomlem1OLD  37266  isdivrngo  37331  iscom2  37376  elrefrels2  37901  elrefrels3  37902  refreleq  37904  elcnvrefrels2  37917  elcnvrefrels3  37918  dnnumch1  42369  aomclem3  42381  aomclem8  42386  rclexi  42947  rtrclex  42949  rtrclexi  42953  cnvrcl0  42957  dfrtrcl5  42961  dfrcl2  43006  csbima12gALTVD  44239  unirnmap  44484  ssmapsn  44492  sge0val  45659  vonvolmbl  45954