Theorem rneq 5910

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

Syntax hints:   → wi 4   = wceq 1559  ^◡ccnv 5644  dom cdm 5645  ran crn 5646

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-opab 5162  df-cnv 5653  df-dm 5655  df-rn 5656

This theorem is referenced by:  rneqi  5911  rneqd  5912  feq1  6665  foeq1  6770  fnrnfv  6922  fconst5  7186  frxp  8101  tz7.44-2  8373  tz7.44-3  8374  ixpsnf1o  8916  ordtypecbv  9462  ordtypelem3  9465  dfac8alem  9982  dfac8a  9983  dfac5lem3  10078  dfac9  10090  dfac12lem1  10097  dfac12r  10100  ackbij2  10195  isfin3ds  10283  fin23lem17  10292  fin23lem29  10295  fin23lem30  10296  fin23lem32  10298  fin23lem34  10300  fin23lem35  10301  fin23lem39  10304  fin23lem41  10306  isf33lem  10320  isf34lem6  10334  dcomex  10401  axdc2lem  10402  zorn2lem1  10450  zorn2g  10457  ttukey2g  10470  gruurn  10753  rpnnen1lem6  12980  relexp0g  15032  relexpsucnnr  15035  dfrtrcl2  15072  mpfrcl  22118  selvval  22153  ply1frcl  22361  pnrmopn  23383  isi1f  25716  itg1val  25725  madeval  27902  axlowdimlem13  29101  axlowdim1  29106  ausgrusgri  29315  0uhgrsubgr  29426  cusgrsize  29601  ex-rn  30588  gidval  30661  grpoinvfval  30671  grpodivfval  30683  isablo  30695  vciOLD  30710  isvclem  30726  isnvlem  30759  isphg  30966  pj11i  31860  hmopidmch  32302  hmopidmpj  32303  pjss1coi  32312  padct  32870  tocyc01  33259  tocyccntz  33285  unitprodclb  33536  esplyfvaln  33832  esplyind  33833  locfinreflem  34098  locfinref  34099  issibf  34591  sitgfval  34599  onvf1odlem3  35412  mrsubvrs  35836  rdgprc0  36105  rdgprc  36106  dfrdg2  36107  brrangeg  36248  poimirlem24  38107  volsupnfl  38128  elghomlem1OLD  38348  isdivrngo  38413  iscom2  38458  elrefrels2  39061  elrefrels3  39062  refreleq  39064  elcnvrefrels2  39077  elcnvrefrels3  39078  dnnumch1  43585  aomclem3  43597  aomclem8  43602  rclexi  44155  rtrclex  44157  rtrclexi  44161  cnvrcl0  44165  dfrtrcl5  44169  dfrcl2  44214  csbima12gALTVD  45436  modelaxreplem1  45518  modelaxreplem2  45519  modelaxrep  45521  unirnmap  45748  ssmapsn  45756  sge0val  46904  vonvolmbl  47199